Research On Spi Calculus-Based Automatic Analyzing Technology Of Cryptographic Protocols

Cryptographic protocols are the secure basis of communication in network and distributed systems. The correctness and security of cryptographic protocols are important to guarantee that attackers can not get secure information or make unfair authentication. But the design of cryptographic protocols is complex and error prone. As results of lack of the research on security requirement of environment, or adoption of unapt technology, there are security flaws in most of cryptographic protocols, and usually they are exposed only when attack exists. But static analysis and manual verification can not find some kinds of bugs or potential attack. So automatic analyzing technology of cryptographic protocols has been one of the hotspots in research of formal cryptographic protocols analyzing in recent years.This paper studies automatic analyzing technology of cryptographic protocols from the point of view of analyzing and implementing. The main works in this paper are listed as follows:(1) An extended Spi calculus is proposed, the definitions about secrecy and authentication of cryptographic protocols are introduced, and the method to automatic analyzing is presented.(2) The type system based on extended Spi calculus is built, type rules are presented, and we proved that the process can not leak any secret datas if it is well-typed in the type system,.(3) By the type system of extended Spi calculus, the secrecy of a typical cryptographic protocol is proved.(4) On the research of automatic analyzing technology based on logic program, an automatic cryptographic protocols analyzer is designed, in which the input syntax is based on extended Spi calculus, and the principle of the analyzer is introduced, and the congruence between the verifier and the type system of extended Spi calculus is proved. Based on security analyzing, the principle of authentication analyzing is presented.(5) The translation rules from the cryptographic protocols described by extended Spi calculus to horn clauses is presented. Automatic translator is designed and implemented, and the automatic translation from the cryptographic protocols described by extended Spi calculus to horn clauses is achieved.