The Formal Analysis Of Cryptographic Protocols

Along with the rapid development and wide application of information technology, the application, Such as E-commerce, becomes more and more popular. So you can imagine how important the information security is. In the network, which is so special and open, if two participants who don't know each other want to have communication, the course must be protected by cryptography.There has been many standpoint of the cryptography protocol's security by now, but none of them has become the standard of the analysis method, so the research of the formalized method of the cryptography protocol is remain the hot topic.First, this thesis introduces some basic knowledge about cryptography, the sort of the cryptography protocol, and some important cryptography technics: en-decryption, data integrity, digital signature, and message authentication. For making the analysis method more efficient, all the protocols of this thesis is analysed under the supposing that the low layer cryptography technics are safe; Then, through analyzing the main standpoint of the protocol analysis, conclude some disadvantages of them. And through analyzing some classical attack to the protocols, conclude the subject of this thesis-the formalize method about cryptography protocols, which depends on Bellare and Rogaway's definition of the protocol's security, and some design principle by the author through the study in these years. This method has 5 modules, First, the protocol is analysed by the first 4 modules, and then its security would be proved by the last module. Through the analysis of many literatures about the provability technic, the author find that the difficulty of the proof of cryptography protocol's security. Therefore, this thesis's proof is based on a logical idea which is different from the classical cryptography's proof. Every step of the proof is accurate. Then, Use the formalize method to test some real communication protocols, such as SSH, Kerberos, and STS. Finally, this thesis sums up the content and make prospect of this field.