The Research Of Formal Verification Method On Cryptography Protocol

Cryptographic Protocol is the base of safe communication of information in open network environment. Its validity plays a key role on network security. In different network applications, a lot of Cryptographic Protocols have been designed and implemented. But it is not easy to design a really safe cryptographic protocol. To ensure the validity of Cryptographic protocol, many kinds of formal methods have been presented to resolve the problem.Current researches on formal verification method focus on logic of belief, algebra method, model checking and so on. Such methods all have their advantages and disadvantages. Though formal methods have already found many attacks toward cryptographic protocol, there are many problems in them, such as too much abstract in verification process, overload with details, hard to locate the problem in protocol and so on.This project constructed a verification method of cryptographic protocol, which contained a logic of belief improved from BAN logic and a target-driven verification strategy of using the logic to verify cryptographic protocol. If the beliefs of the principals are in accordance with the fact, the validity of cryptographic protocol is ensured.The logic presented in this document can express the beliefs of both principals and the information known by the attacker, and can represent the attack in cryptography security area. The target-driven reversing verification method uses the mechanism of reverse reasoning, and reduces the searching space of attacking trace, meaning high efficiency.This document verified A(0) protocol and Needham-Schroeder public key protocol with the reversing verification method, with the reasoning process and attacking trace being given and the protocol problem being located. Such case study demonstrated the ability of the target-driven reversing verification method in verifying cryptographic protocol.The further study will focus on extending the logic presented in this document to apply it on other areas of cryptographic protocol successfully, such as electronic payment protocol, security mail protocol and so on.