基于逻辑的电子商务协议属性的分析与研究
|
摘要
电子商务是当前各国研究发展的热点，电子商务的普及与接受取决于以下属性的解决：安全、原子、隐私与匿名，它以电子商务协议为构成框架，而电子商务协议是决定电子商务发展的关键因素，形式化描述和分析电子商务协议并验证它们的属性的有效方法。研究电子商务协议及其安全性，对于我们设计安全的电子商务协议和促进电子商务协议的发展很有帮助。
作为形式化分析方法的一种，逻辑分析方法是迄今为止使用最为广泛的一种方法。就是在安全协议的形式化分析中运用模态逻辑，这一点类似于分布式系统中对知识和信仰演变的分析中的逻辑。此逻辑是由许多不同的声明和参考规则组成的，其中声明是关于分布式系统消息的一些信仰或知识的，而参考规则是由从其它信仰到新信仰或从旧知识及信仰到新知识中导出的，前者符合信仰逻辑，而后者是相应的知识逻辑。信仰逻辑局限于协议验证属性的分析上。其中BAN逻辑在分析安全协议中获得了巨大的成功。
在本文中，作者主要研究了BAN逻辑和其相关扩展逻辑及其缺陷，并说明其分析协议的方法、步骤，研究了它的分析协议的优势和缺陷，然后结合它们的扩展逻辑，引用了一种新的分析电子商务协议属性的形式化逻辑语言，该语言逻辑性强、应用简易，作者还简单介绍了一种小金额的交易协议——NetBill协议，并对其有入侵者的情况下的属性进行了逻辑抽象，最后用作者提出的逻辑对抽象化的NetBill协议属性进行了完全的分析与验证，证实了逻辑是有效和成功的。
Currently, electronic commerce is the heat point of the research and development in each country, Popularization and acceptance of electronic commerce mainly depends on solution of the following properties: security, atomic, privacy and anonymity. Electronic commerce protocol is the comprising framework of electronic commerce, and its security is the key factor to decide the development of electronic commerce. Formal description and analysis are an efficient way to describe electronic commerce protocol and verify their properties. The research in electronic commerce protocols and their security is helpful for designing safe electronic commerce protocols and promoting the development of electronic commerce.
Modal logic, as one of formal methods, is perhaps the best known and most influential method, which consists of various statements about belief in or knowledge about messages in a distributed system, as well as inference rules for deriving new beliefs from available belief and /or new knowledge from available knowledge and beliefs. The former corresponds to logic belief, while the latter logic of logic knowledge is useful in analyzing the properties of protocols. BAN is one of logics that got a big frame for its success in analyzing security protocols.
In this paper, BAN logic and the extended BAN logic are primarily introduced, and studied in their advantages and weakness. Combing the advantages, we apply a new formal logic language to analyze electronic commerce protocol and their properties. The language has a strong logic and can be applied easily. A famous
electronic micro-payment protocol--NetBill protocol is also simply introduced and
abstracted , At last, the abstracted protocol is especially analyzed and verified completely by the new logic.
作为形式化分析方法的一种，逻辑分析方法是迄今为止使用最为广泛的一种方法。就是在安全协议的形式化分析中运用模态逻辑，这一点类似于分布式系统中对知识和信仰演变的分析中的逻辑。此逻辑是由许多不同的声明和参考规则组成的，其中声明是关于分布式系统消息的一些信仰或知识的，而参考规则是由从其它信仰到新信仰或从旧知识及信仰到新知识中导出的，前者符合信仰逻辑，而后者是相应的知识逻辑。信仰逻辑局限于协议验证属性的分析上。其中BAN逻辑在分析安全协议中获得了巨大的成功。
在本文中，作者主要研究了BAN逻辑和其相关扩展逻辑及其缺陷，并说明其分析协议的方法、步骤，研究了它的分析协议的优势和缺陷，然后结合它们的扩展逻辑，引用了一种新的分析电子商务协议属性的形式化逻辑语言，该语言逻辑性强、应用简易，作者还简单介绍了一种小金额的交易协议——NetBill协议，并对其有入侵者的情况下的属性进行了逻辑抽象，最后用作者提出的逻辑对抽象化的NetBill协议属性进行了完全的分析与验证，证实了逻辑是有效和成功的。
Currently, electronic commerce is the heat point of the research and development in each country, Popularization and acceptance of electronic commerce mainly depends on solution of the following properties: security, atomic, privacy and anonymity. Electronic commerce protocol is the comprising framework of electronic commerce, and its security is the key factor to decide the development of electronic commerce. Formal description and analysis are an efficient way to describe electronic commerce protocol and verify their properties. The research in electronic commerce protocols and their security is helpful for designing safe electronic commerce protocols and promoting the development of electronic commerce.
Modal logic, as one of formal methods, is perhaps the best known and most influential method, which consists of various statements about belief in or knowledge about messages in a distributed system, as well as inference rules for deriving new beliefs from available belief and /or new knowledge from available knowledge and beliefs. The former corresponds to logic belief, while the latter logic of logic knowledge is useful in analyzing the properties of protocols. BAN is one of logics that got a big frame for its success in analyzing security protocols.
In this paper, BAN logic and the extended BAN logic are primarily introduced, and studied in their advantages and weakness. Combing the advantages, we apply a new formal logic language to analyze electronic commerce protocol and their properties. The language has a strong logic and can be applied easily. A famous
electronic micro-payment protocol--NetBill protocol is also simply introduced and
abstracted , At last, the abstracted protocol is especially analyzed and verified completely by the new logic.
引文
[1] 徐建敏，王莹．电子商务的安全问题．河南大学学报(自然科学版)，2002，32(3)：101-103．
[2] 方美琪．电子商务概论[M]．北京：清华大学出版社，2000．
[3] 周展飞，周典萃，王贵林，卿斯汉．电子商务协议的公平性．电子学报，2000，28(9)：13-15．
[4] 杜习英，刘晓云，电子商务教程[M]安徽：安徽科学技术出版社，2001，36-56．
[5] 黄敏学，电子商务[M]北京：高等教育出版社，2000，205-217．
[6] Larry Loeb. Secure Electronic Transactions Introduction and Technical Reference.ARTECH, INC, 1998
[7] 吕廷杰 电子商务教程[M]北京：电子工业出版社，2000，47-67．
[8] Netscape Secure Socket Layer[EB/OL].http://home.netscape.com/eng/ss13/,2002.5
[9] SET Co. SET Secure Electronic Transaction Specification: Formal Protocol Definition, May 1997. Available electronically at http://www.setco.org/set_specifi cations.html.
[10] 杨晋吉，苏开乐．电子商务中安全协议的验证方法．计算机工程与应用．2003，19：146-149．
[11] 杨红丽．形式化方法(FM)．西安邮电学院学报．1999年6月第4卷第2期．：3～4．
[12] BurrowsM,AbadiM,NeedhamRM.ALogicof Authentication[R].TechnicalReport 39,CANADA:DEC Systems Research Center,1989.Partsand Versionsof ThismaterialHave Been Presentedin Many Places Including ACM Transactionson Computer Systems,1990,8(1):18～36.
[13] 束妮娜，王亚弟．认证协议的形式逻辑分析方法——BAN类逻辑综述，计算机应用研究．2002．19：2-3．
[14] 余冬梅，边培泉，冯涛．安全协议中的形式化验证技术．微机发展．2003，13(11)：112-114．
[15] 鲍峥嵘、虞慧群、邵志清、宋国新．铁路系统的模型检查和参数分析．华东理工大学学报．1999，25(21)：4～5．
[16] ClarkeE, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specification[J].ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.
[17] Theory Generation for Security Protocols. Darrell Kindred, Jeannette M.Wing. http://www-2.cs.cmu.edu/afs/cs/project/calder/www/TG.html.1999.06.16
[18] 张玉清，李继红，肖国镇．密码协议分析工具——BAN逻辑及其缺陷．西安电子科技大学学报．1999，26(3)：376-378．
[19] 张萌，许剑卓，左英男．类BAN逻辑的两个重要缺陷．计算机工程．2000，26(7)：133-135．
[20] 冯彬．关于BAN逻辑分析的改进．中国科学院研究生院学报．2002,19(3)：306-310．
[21] Kailar R. Accountability in electronic commerce protocols. IEEE Transactions on Software Engineering,1996,22(5):313～328.
[22] 周典萃，卿斯汉，周展飞．Kailar逻辑的缺陷．软件学报．1999，10(12)：1238-1245．
[23] Michael B, Martin Abadi, Roger Needham. A logic of authentication.ACM Transactions on Computer System,1990,8(1):18～36.
[24] 白硕，隋立颖，陈庆锋，付岩，庄超．安全协议的验证逻辑．软件学报．2000，11(2)：213-221．
[25] Abadi M, Tuttle M.A semantics for logic of authentication. In: Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing Montreal: ACM Press,1991.201～216.
[26] Kailar R, Gligor V. On belief evolution in authentication protocols. In: Catherine Harris, Madallum A C eds. Proceedings of 4th IEEE Computer Security Foundations Workshop.Los Alamitors, CA:IEEE Computer Society Press,1991.103～116.
[27] Volker Kessler, Cabriele Wedel. AUTLOG——an advanced logic of authentication. In: Bob Wernereded. Proceedings of the 7th IEEE Computer Security Foundations Workshop. Los Alamitors, CA: IEEE Computer Society Press, 1994.90～99.
[28] Kailar R. Accountability in electronic commerce protocols. Proceedings of IEEE Transactions on Software Engineering,1996,22(5):313～3286.
[29] 许剑卓，戴英侠，左英男．类BAN逻辑基本模型及缺陷．软件学报．2000,11(12)：1160-1165．
[30] Mao, Wen-bo, Boyd, C. Towards a formal analysis of security protocols. In:Jackson, Red. Proceedings of the Computer Security Foundations Workshop Ⅵ. Los Alamitos,CA:IEEE Computer Society Press,1991.147～158.
[31] Li, Gong, Need Ham, R, Yahalom, R. Reasoning about belief in cryptographic protocols. In: Mike, C.C., ed. Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos,CA:IEEE Computer Society Press,1990.234～248.
[32] Syverson, P. F., van O orschot, P.C.On unifying some cryptographic protocol logics. In: Oakson, N. ed. Proceedings of the 1994 IEEE Computer Societ Symposium on Research in Security and Privacy.Los Alamitos: IEEE Computer Society Press.1994.109～121.
[33] M. Debbabi, M. Mejri, N. Tawbi, I. Yahmadi. Formal automatic, verification of authentication cryptographic protocols.1997 Proceedings, First IEEE International Conference on Format Engineering Methods, Page(s): 50-59,1997.
[34] P Van Oorschot. Extending Authentication Logics of Authentication Logic of Belief to Key Agreement Protocols[C].In Proceedings of the First ACM Conference on Computer and Communications Scurity,1993,232-243.
[35] Paul Syverson, et al. On Unifying Some Authentication Protocol Logics[C]. In IEEE Computer Society Symposium on Research in Security and Privacy, IEEE Computer Society, 1994,14-28.
[36] Kessler V, Wedel G.AUTLOG——An Advanced Logic of Authentication[A]. In Proc of the Computer Security Foundations Workshop [C].USA:IEEE Computer Society Press,1994.90～99.
[37] Neuman B C, Medvinsky G. Requirements for network payment: The exchequer perspective. In: Proc of IEEE COMPCON'95. 1995.
[38] Tygar JD. Atomicity in electronic commerce. In: Proc of the 15th Annual ACM Symposium on Principles of Distributed Computing.1996.8～26.
[39] Camp J, Harkavy M, Tygar JD et al. Anonymous atomic transactions. In: Proc of 2nd Use nix Workshop on Electronic Commerce.1996.123～133.
[40] 陆钟万著，面向计算机科学的数理逻辑[M]．北京：科学出版社，2002．
[41] Cox, B. maintaining privacy in electronic transactions. Technical Report. T R1994-8,Information Networking Institute, 1994.
[42] Cox, B.Tygar, J.D.Sirbu, M. Netbill security and transaction protocol. In Proceeding of the 1st USENIX workshop on electronic Commerce.1995,77-88.
[43] http://www.netbill.com/.
[44] Domingo-Ferrer, J, Herrea-Joancomarti, J.Ananonymous electronic commerce scheme with an off-line authority and untrusted agents. SIGMOD Record, 1998,27(4): 62-67.
[45] Gray, J. Notes on database operating systems. In: Bayer, R. Graham, R, M, Seeg Muller, eds.operating Systems: an advanced Course. Springer Verlag, 1978.
[46] 冯涛，余冬梅，边培泉．NetBill协议的形式化描述及分析．兰州理工大学学报．2004年第四期．
[47] CoxB,TygarJ.DsirbuM.NetBill Security and Transaction Protocol[EB/OL]. http://citeseer.nj.neccom/cox95netbill.html, 2002-03-02/2003-05-07.
[48] 左英男，戴英侠，许剑卓．一种安全的Internet小额交易协议分析[J]．计算机工程，2000，26(7)：136-138．
[49] LU MA and JEFFREY JP.TSAI. Formal verification Techniques for Computer Communication Security [EB/OL]. http://citeseer.nj.nec.com/463674.html, 2003-01-06/2003-05-12.
[50] 古天龙．形式化技术及其工业应用：现状与展望．桂林电子工业学院学报．第20卷第4期2000年12月．
[2] 方美琪．电子商务概论[M]．北京：清华大学出版社，2000．
[3] 周展飞，周典萃，王贵林，卿斯汉．电子商务协议的公平性．电子学报，2000，28(9)：13-15．
[4] 杜习英，刘晓云，电子商务教程[M]安徽：安徽科学技术出版社，2001，36-56．
[5] 黄敏学，电子商务[M]北京：高等教育出版社，2000，205-217．
[6] Larry Loeb. Secure Electronic Transactions Introduction and Technical Reference.ARTECH, INC, 1998
[7] 吕廷杰 电子商务教程[M]北京：电子工业出版社，2000，47-67．
[8] Netscape Secure Socket Layer[EB/OL].http://home.netscape.com/eng/ss13/,2002.5
[9] SET Co. SET Secure Electronic Transaction Specification: Formal Protocol Definition, May 1997. Available electronically at http://www.setco.org/set_specifi cations.html.
[10] 杨晋吉，苏开乐．电子商务中安全协议的验证方法．计算机工程与应用．2003，19：146-149．
[11] 杨红丽．形式化方法(FM)．西安邮电学院学报．1999年6月第4卷第2期．：3～4．
[12] BurrowsM,AbadiM,NeedhamRM.ALogicof Authentication[R].TechnicalReport 39,CANADA:DEC Systems Research Center,1989.Partsand Versionsof ThismaterialHave Been Presentedin Many Places Including ACM Transactionson Computer Systems,1990,8(1):18～36.
[13] 束妮娜，王亚弟．认证协议的形式逻辑分析方法——BAN类逻辑综述，计算机应用研究．2002．19：2-3．
[14] 余冬梅，边培泉，冯涛．安全协议中的形式化验证技术．微机发展．2003，13(11)：112-114．
[15] 鲍峥嵘、虞慧群、邵志清、宋国新．铁路系统的模型检查和参数分析．华东理工大学学报．1999，25(21)：4～5．
[16] ClarkeE, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specification[J].ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.
[17] Theory Generation for Security Protocols. Darrell Kindred, Jeannette M.Wing. http://www-2.cs.cmu.edu/afs/cs/project/calder/www/TG.html.1999.06.16
[18] 张玉清，李继红，肖国镇．密码协议分析工具——BAN逻辑及其缺陷．西安电子科技大学学报．1999，26(3)：376-378．
[19] 张萌，许剑卓，左英男．类BAN逻辑的两个重要缺陷．计算机工程．2000，26(7)：133-135．
[20] 冯彬．关于BAN逻辑分析的改进．中国科学院研究生院学报．2002,19(3)：306-310．
[21] Kailar R. Accountability in electronic commerce protocols. IEEE Transactions on Software Engineering,1996,22(5):313～328.
[22] 周典萃，卿斯汉，周展飞．Kailar逻辑的缺陷．软件学报．1999，10(12)：1238-1245．
[23] Michael B, Martin Abadi, Roger Needham. A logic of authentication.ACM Transactions on Computer System,1990,8(1):18～36.
[24] 白硕，隋立颖，陈庆锋，付岩，庄超．安全协议的验证逻辑．软件学报．2000，11(2)：213-221．
[25] Abadi M, Tuttle M.A semantics for logic of authentication. In: Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing Montreal: ACM Press,1991.201～216.
[26] Kailar R, Gligor V. On belief evolution in authentication protocols. In: Catherine Harris, Madallum A C eds. Proceedings of 4th IEEE Computer Security Foundations Workshop.Los Alamitors, CA:IEEE Computer Society Press,1991.103～116.
[27] Volker Kessler, Cabriele Wedel. AUTLOG——an advanced logic of authentication. In: Bob Wernereded. Proceedings of the 7th IEEE Computer Security Foundations Workshop. Los Alamitors, CA: IEEE Computer Society Press, 1994.90～99.
[28] Kailar R. Accountability in electronic commerce protocols. Proceedings of IEEE Transactions on Software Engineering,1996,22(5):313～3286.
[29] 许剑卓，戴英侠，左英男．类BAN逻辑基本模型及缺陷．软件学报．2000,11(12)：1160-1165．
[30] Mao, Wen-bo, Boyd, C. Towards a formal analysis of security protocols. In:Jackson, Red. Proceedings of the Computer Security Foundations Workshop Ⅵ. Los Alamitos,CA:IEEE Computer Society Press,1991.147～158.
[31] Li, Gong, Need Ham, R, Yahalom, R. Reasoning about belief in cryptographic protocols. In: Mike, C.C., ed. Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos,CA:IEEE Computer Society Press,1990.234～248.
[32] Syverson, P. F., van O orschot, P.C.On unifying some cryptographic protocol logics. In: Oakson, N. ed. Proceedings of the 1994 IEEE Computer Societ Symposium on Research in Security and Privacy.Los Alamitos: IEEE Computer Society Press.1994.109～121.
[33] M. Debbabi, M. Mejri, N. Tawbi, I. Yahmadi. Formal automatic, verification of authentication cryptographic protocols.1997 Proceedings, First IEEE International Conference on Format Engineering Methods, Page(s): 50-59,1997.
[34] P Van Oorschot. Extending Authentication Logics of Authentication Logic of Belief to Key Agreement Protocols[C].In Proceedings of the First ACM Conference on Computer and Communications Scurity,1993,232-243.
[35] Paul Syverson, et al. On Unifying Some Authentication Protocol Logics[C]. In IEEE Computer Society Symposium on Research in Security and Privacy, IEEE Computer Society, 1994,14-28.
[36] Kessler V, Wedel G.AUTLOG——An Advanced Logic of Authentication[A]. In Proc of the Computer Security Foundations Workshop [C].USA:IEEE Computer Society Press,1994.90～99.
[37] Neuman B C, Medvinsky G. Requirements for network payment: The exchequer perspective. In: Proc of IEEE COMPCON'95. 1995.
[38] Tygar JD. Atomicity in electronic commerce. In: Proc of the 15th Annual ACM Symposium on Principles of Distributed Computing.1996.8～26.
[39] Camp J, Harkavy M, Tygar JD et al. Anonymous atomic transactions. In: Proc of 2nd Use nix Workshop on Electronic Commerce.1996.123～133.
[40] 陆钟万著，面向计算机科学的数理逻辑[M]．北京：科学出版社，2002．
[41] Cox, B. maintaining privacy in electronic transactions. Technical Report. T R1994-8,Information Networking Institute, 1994.
[42] Cox, B.Tygar, J.D.Sirbu, M. Netbill security and transaction protocol. In Proceeding of the 1st USENIX workshop on electronic Commerce.1995,77-88.
[43] http://www.netbill.com/.
[44] Domingo-Ferrer, J, Herrea-Joancomarti, J.Ananonymous electronic commerce scheme with an off-line authority and untrusted agents. SIGMOD Record, 1998,27(4): 62-67.
[45] Gray, J. Notes on database operating systems. In: Bayer, R. Graham, R, M, Seeg Muller, eds.operating Systems: an advanced Course. Springer Verlag, 1978.
[46] 冯涛，余冬梅，边培泉．NetBill协议的形式化描述及分析．兰州理工大学学报．2004年第四期．
[47] CoxB,TygarJ.DsirbuM.NetBill Security and Transaction Protocol[EB/OL]. http://citeseer.nj.neccom/cox95netbill.html, 2002-03-02/2003-05-07.
[48] 左英男，戴英侠，许剑卓．一种安全的Internet小额交易协议分析[J]．计算机工程，2000，26(7)：136-138．
[49] LU MA and JEFFREY JP.TSAI. Formal verification Techniques for Computer Communication Security [EB/OL]. http://citeseer.nj.nec.com/463674.html, 2003-01-06/2003-05-12.
[50] 古天龙．形式化技术及其工业应用：现状与展望．桂林电子工业学院学报．第20卷第4期2000年12月．