This paper introduces the payment process of SET(secure electronic transactions)protocol,and extends the logical framework of NDL to fit the purpose of logical verification of SET.This means to add some new axioms about SET protocols and redefine some given inference rules.Based on these,the logical verification for key fragments of SET protocol is given to show the importance of NDL and its extensions in E-commerce.Topics for further research on the “Rule of Accumulation” are also proposed.
[1]SET Secure Electronic Transaction Specification.Book 1:Business Description Version 1.0.May 31,1997
[2]SET Secure Electronic Transaction Specification.Book 2:Programmer's Guide Version 1.0.May 31,1997
[3]Burrows M,Abadi M,Needham R.A logic of authentication.ACM Transactions on Computer System,1990,8(1):18~36
[4]Abadi M,Tuttle M.A semantics for a logic of authentication.In:Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing.Montreal:ACM Press,1991.201~216
[5]Kessler V,Wedel C.AUTLOG——an advanced logic of authentication.In:Wernered B ed.Proceedings of the 7th IEEE Computer Security Foundations Workshop.Los Alamitors,CA:IEEE Computer Society Press,1994.90~99
[6]Kailar R.Accountability in electronic commerce protocols.Proceedings of the IEEE Transactions on Software Engineering,1996,22(5):313~328
[7]Bai Shuo,Sui Li-ying,Chen Qing-feng et al.Authentication logic for secure protocols.Journal of Software,2000,11(2):213~221
(白硕,隋立颖,陈庆锋等.安全协议的验证逻辑.软件学报,2000,11(2):213~221)