Research On Automatically Formal Analysis For Security Protocols Based On Probabilistic Polynomial-time Process Calculus

The design and verification of security protocols play important roles in information security field. Formal verification of security protocols with automated tools is a powerful technology. The research in the methods of formal analysis for security protocols is a hot topic today. Formal methods place into two categories: symbolic method and computational method. In symbolic method, the cryptographic primitives serve as perfect black boxes. Computational method is based on computational complexity and probability theory; it can create a reliable proof of cryptography.Deniable authentication protocol is a kind of security protocol which is widely used in e-government. The traditional proof of deniability based on symbolic method, it is manual and prone to error, and it cannot establish cryptography reliability. This paper introduces a probability model based on a kind of probabilistic polynomial-time process calculus: Blanchet calculus. Analyze and prove the deniability of deniable authentication protocol using this process calculus. Main works are as follows:(1) A complete overview on technology of the formal methods. Focus on the theory of security protocols and analysis techniques.(2) Firstly introduce computational method, Blanchet calculus and CryptoVerif in detail, including syntax and non-formal semantics, type systems, formal semantics, observation equivalence, Game conversion, and give a simple example. Then proposed a deniable model based on Blanchet calculus. Apply this model to the proof of Fan et al deniable authentication protocol.(3) Based on elliptic curve discrete logarithm problem; present a non-interactive deniable authentication protocol. Analyze and prove the deniability of this protocol using the proposed deniable model, Blanchet calculus and CryptoVerif.