Design And Implementation Of Description Model For Provable Security Automatic Analyse Of Public-key Cryptographic Schemes

Provable security is important in evaluating the security of cryptographic protocols, while manual proof is fallible and hard to estimate. Construct sequence of games with the help of computers and then actualize the automatic security proof is a feasible method. In this thesis, we make deep research on the automatic security proof technique based on sequence of games and the realization of automatic analyzing system, the main content includes:Firstly, we make research on the method of cryptographic protocols automatic security proof based on sequence of games and the process calculus, design the probability process calculus language and then bring forward the formalizing description model of cryptographic protocols. The model can formalize the attack course of cryptographic protocol and the security goal. It can also well describe the intercurrent features of attack game in the theory of provable security, while the probability semantics depicts the changes of the adjacent games.Secondly, based on the formal description model we define the input file criterion of automatic cryptographic protocols analyzing system. The user can describe the initial attack game, transition rules, and anticipant security goals and so on with it. This syntax rules is simple and easy to use and read for the user.Thirdly, with the defined describing specification and data structure that the system can handle, we design and implement a parser with the tools of LEX and YACC. The parser can turn the input file into initial data structure of the system, and provide basis for the automatic provable security proof.Finally, we design the architecture of automatic analyzing system, and introduce the dynamic depth-first state tree traversal algorithm to devise the control strategy of automatic provable security system which can schedule every transition module and at last make the automatically analysis of provable security come true.The results of this thesis have been used in "automatic provable security analyzing system of cryptographic protocols. At present, this system can handle the automatic security proof of some classic cryptographic algorithms (such as the FDH signature algorithm and ElGamal encryption algorithm).