Research On Automatic Security Proof Approach Of Public-key Cryptographic Schemes Based On Process Calculus

Provable security is an important criterion for evaluating the security of cryptographic schemes at present. However, manual proofs are difficult, prone to errors and hard to estimate. The automatic proof with the help of the computers is an effective approach to solve this problem. In this thesis, we make deep research and analysis on the automatic security proof approach of public-key cryptographic schemes and build an automatic provable security analyzing system based on the academic model that can handle the automatic security proof of the public-key cryptographic schemes.The main content includes:(1) Bring forward the idiographic actualizing method of reduction based on game transitions. This paper adopts the game-based approach to make the reduction between cryptographic scheme and mathematical difficult problem come true and uses the sequence of games to organize the security proof course. We use the syntactic transitions and transitions based on cryptographic primitives or security assumptions to obtain the sequence of games begin with the initial attack game.(2) Design a formalizing description model. We Compare the two head models for analyzing the security of protocols: symbolic model and computational model, and then choose the computational model to be the basic model of security proof for that it's much more realistic and less abstract. The proof course of computational model is very fussy and hard to automatically actualize, so we import the process calculus into the computational model and design a formalizing model which can satisfy the automatic security proof of the cryptographic schemes. That is the precondition of automatic provable security analysis.(3) Define a sort of advanced describing language. It's defined based on the formalizing description model. Users use this kind of language to describe the cryptographic algorithms and the anticipant security goals. This is also the input file of the automatic security analyzing system. The input file parsed by the parser and then form the initial attack game that formalized by process calculus language to carry through the transition proof.(4) Introduce the notion of observational equivalence, the conformation and probability calculating technique of the observational equations. The observational equivalence is the useful academic gist for constructing the sequence of games. The observational equations can formalize the cryptographic primitives and security assumptions and the transitions based on it make automatically receive the sequence of games happen.(5) Distill the identical equations and observational equations from the properties of cyclic group and prove the security of ElGamal encryption and its hashed version with the automatic security analyzing system. Because the observational equations are based on the security properties of cryptographic primitives and the assumptions of algorithms can be reused, we actually enrich the storeroom of the transition rules. This makes sense for the proof of other cryptographic protocols with the similar cryptographic properties.Finally, the conclusions of the whole thesis are summed up and the future research is proposed.