Study On The Computationally Sound Verification Of Security Protocols

With the development of Internet, information security is becoming more and moreimportant. How to provide the confidentiality, integrity, availability and non-repudiationof data through the open network turns into hot topics. Among all the solutions, securityprotocol is one of the most effective methods. But because of the openness of Internetand high concurrency of protocols, designing and analyzing of security protocols is verydifficult. Now the main approach for guaranteeing the security of the protocols is formalverification technology.For the last 30 years, there are two main types of approaches in security protocolanalysis domain. The first type is called symbolic methods, which use abstraction formodelingprotocolmessages,adversariesandcryptographicalgorithms. Thoughsymbolicapproaches are easy to use, they have problems of unsoundness: sometimes the abstrac-tion is too ideal and when the real protocols run differently from the abstract protocols,protocols that are proved secure in symbolic model may be vulnerable when they are im-plemented. The other type is called computational methods, which model protocols hon-estly in the computational models, and use provable security. They are thought to be thesound in verification. However, because of the probabilistic and computational problemsin the verification, the proof procedures are very complicated and prone to errors.Now, how to combine the advantages of the symbolic and computational approachesto get an approach which is both easy to use and sound becomes a hot topic. Followingthe research direction, this dissertation studies the extension of existing verification ap-proaches, modeling in the computational model, computationally sound qualitative meth-ods and computationally sound quantitative methods. The primary contributions can besummarized as following:1) Extending and analyzing the mechanized verification tool CryptoVerif. Firstly,we extend the capability of a famous tool CryptoVerif, to enable it to prove the Zhou-Gollmann non-repudiation and Diffie-Hellman protocols. We first prove the security ofZhou-Gollmann and Diffie-Hellman based Kerberos protocols automatically in the com-putational model. Secondly, we find some deficiencies in prior works, and correspondingremedy methods are proposed. Lastly, the modeling of CryptoVerif for modeling secu- rity protocols and cryptographic algorithms is analyzed, and a research line of presentingcomputational logic is proposed.2) Approachesformodelingsecurityprotocolsinthecomputationalmodel. Firstly,a calculus in the computational model is defined, which can be used to model the ac-tions of parties in the security protocols precisely. Based on the calculus, the verificationlogic is proposed and semantics are interpreted in the computational model. Secondly, theNeedham-Scheoder-Lowe and Challenge-Response protocols are modeled with the cal-culus. Thirdly, the calculus is compared with the Computational Protocol CompositionalLogic (CPCL). And we found that our calculus is more accurate, and can describe moreprotocol actions, such as key querying and the association between parties and keys.3) Computationally sound qualitative verification. Firstly, a proof system con-taining first-order axioms, cryptographic axioms and other axioms is established and thesoundness is proved. Compared with other logic axiom systems, our axiom system canmodel the security notions of random number generation, symmetric encryption, pub-lic key encryption, public key signature and message authentication code. Secondly, theproof capability of the axiom is compared with CPCL. We find that there is a mistake inthe model of CPCL, which does not exist in our proof system. Furthermore, our proofsystem contains temporal attributes, and is more suitable for analyzing security protocols.Thirdly, by proving the mutual authentication property of NSL with the proof system, thevalidity of the approach is tested.4) Computationally sound quantitative verification methods. Firstly, we extend thequalitative verification approach with probabilities, and establish a quantitative deductionsystem. Compared with CryptoVerif and classic Adam's probabilistic logic, our quantita-tive system is based on the explicit definition of probabilistic events, and more suitablefor verification of security protocols. Secondly, we analyze the possibility of extendingCPCL with probabilities, and point out the difficulties in doing this. Lastly the Challenge-Response protocol is verified with the system, and the results are analyzed.