Chinese Journal of Computers   Full Text
Title	The Automatic Verification and Improvement of SET Certificate Registration Protocols with SPV
Authors	XIAO Yin-Yin1) SU Kai-Le1),2) YUE Wei-Ya1) CHEN Qing-Liang3) LU Guan-Feng4) YANG Jin-Ji1),5)
Address	1)(Key Laboratory for Information Security of Guangdong Province, School of Information Science & Technology, Sun Yat-Sen University, Guangzhou 510275) 2)(Key Laboratory for High Confidence Software Technologies of Ministry of Education, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871) 3)(Department of Computer Science, Jinan University, Guangzhou 510632) 4)(College of Computer Science, Beijing University of Technology, Beijing 100022) 5)(School of Computer Science, South China Normal University, Guangzhou 510631)
Year	2008
Issue	No.6(1035—1045)
Abstract &   Background	Abstract Based on the Instantiation Space Logic theory and knowledge reasoning, the authors implement the totally automatic verification on the complete SET certificate registration protocols’ authentication and secrecy properties using SPV, and improve the protocols. SPV can efficiently verify whether the security protocol satisfies the goals in CAPSL(Common Authentication Protocol Specification Language) as well as multi-level epistemic specifications using modern SAT solvers. All protocols should be simplified before being verified by logics or tools. As to the SET protocols, it is the most complex industrial protocol at present, which has the document of over 1000 pages. Therefore, it is very difficult to simplify and there are few research works about it. Besides, some existent simplified models are not complete enough.Consequently, the paper gives a simplified model which is more close to the original SET certificate registration protocols, and introduces the model’s formal description in SPV with the verification process and results. Moreover, according to the hidden danger of the protocols brought by the unsatisfied epistemic specification, the authors improve the protocols and show the effectiveness. The work also justifies that SPV has the ability to deal with complex industrial protocols. Keywords SET certificate registration protocols; automatic verification; SPV; authentication; secrecy Background This research is supported by the National Basic Research 973 Program of China under grant No.2005CB321902, the National Natural Science Foundation of China under grant Nos.60496327, 10410638, 60473004, the Natural Science Foundation of Guangdong under grant No.06023195 and the Natural Science Foundation Team Collaboration Project of Guangdong under grant No.04205407. It is widely acknowledged that logical flaws in security protocols, especially in complex industrial protocols, are hard to analyze. Instantiation Space Logic is a new justification-oriented security protocol logic under Dolev-Yao model, which can prove whether a protocol satisfies concerned security properties. The tool of this logic SPV(Security Protocol Verifier) is designed and implemented, which can efficiently verify whether the security protocol satisfies the goals in CAPSL(Common Authentication Protocol Specification Language) as well as multi-level epistemic specifications using modern SAT solvers. All protocols should be simplified before being verified by logics or tools. SET(Secure Electronic Transaction) protocol is an e-commerce protocol devised by Visa and MasterCard. At present, it is the most complex industrial protocols, which has the document of over 1000 pages. Therefore, it is very difficult to simplify and there are few research works about it. Besides, some existent simplified models are not complete enough. For example, some models do not describe the XOR calculus, while the attacks in some others are not realistic. In this paper, based on the Instantiation Space Logic theory and knowledge reasoning, the authors give a simplified model which is more close to the original SET certificate registration protocols than before, and introduce the model’s formal description in SPV with the verification process and results. Moreover, according to the hidden danger of the protocols brought by the unsatisfied epistemic specification, the authors improve the protocols and show the effectiveness. Actually, whether a theory or tool can verify SET protocol has become a standard to demonstrate whether the verification technology is mature enough to cope with the complex industrial protocols. Some parts of this protocol have been verified by model checkers or semi-automatic proves such as Paulson’s Isabelle. However, this work is the first one to implement the totally automatic verification on the complete SET certificate registration protocols’ authentication and secrecy properties, so it justifies that SPV has the ability to deal with complex industrial protocols.