Modeling And Verifying Complex Security Protocols

With the development of network, security problems in the internet are becomingmore and more urgent and important. Security properties encounter more and more chal-lenges. Security protocol is one of e?ective methods to solve the internet security issues.The open internet with security protocols can realize various security functions, such asidentity authentication etc. Since participants of communication cannot find the real iden-tity of each other by biometric features in computer network, the mutual authenticationshould be founded on cryptography. Security protocol is a type of communication protocolbased on cryptography, which runs over the computer network or distributed systems, andarranges the execution steps and the execution rules with the cryptographic algorithmsamong the participants who implement tasks such as key distribution, identity authenti-cation, e-commerce transaction, etc. The correctness of security protocols is critical forthe transactions over the open networks. However, security protocols designed and usedin the real world do not always achieve their objectives. Many protocols have been foundhaving ?aws after a long application period.It's a hot field in formal method to design and develop an e?cient automatic toolfor the verification of security protocols, and it's an important step in verification of com-plex security protocols. Based on Horn logic model given by Bruno Blanchet, this thesisperforms a systematic and deep study of protocol verification, algorithms for construct-ing counterexamples and complex protocols. The main task includes the following threeaspects:1. Algorithms for constructing counterexamples automatically of security protocols basedon Horn logic.Bruno Blanchet presents the security protocols'model based on Horn logic, whichcan verify security protocols e?ectively. In order to add role information of messageinto Horn model, this thesis designs corresponding data structures, and proposesimplementation of algorithms for constructing counterexamples automatically, so thatthe verification tool can automatically construct the standard form of counterexamplesfrom resolution sequences unsatisfied with security properties. This way is helpful toverify protocols with verification tools on Horn logic.2. Prediction for non-termination of fix-point computation. Non-termination of verification of security protocols can be derived from thenon-termination of fix-point computation. Having investigated the characteristic ofnon-termination of fix-point computation on the logic program model of security pro-tocols, this thesis gives a method to predict whether the fix-point computation isnon-terminated. Based on this method, it is possible to adaptively select a right (exact or abstract ) verification mode to verify (terminate or non-terminated) securityprotocols.3. Abstraction and iterative refinement framework.The problem of correctness verification for security protocols is undecidable, butit is feasible to verify protocols by abstract interpretation. By investigating charac-teristics of Horn logic model, this thesis presents a framework to combine securityprotocol verification and abstraction with refinement. Abstract verification guaran-tees termination and refinement can remove false counterexamples, so this abstrac-tion and iterative refinement framework can also work for non-terminated protocolsin Horn logic model. To improve the precision of abstract model, this thesis proposeslocal abstraction and refinement in the framework. It is more e?ective to verify non-terminated security protocols by local abstraction than by global abstraction. Theresult shows that this is another e?ective way to verify complex protocols.4. Modeling and verifying time sensitive security protocols.By adding time events into process algebra model, in this thesis, time stampscan be described e?ectively in protocol model. And then, by appending linear con-straints on time variables to Horn logic model of security protocol, the extended Hornlogic model can deal with time information e?ciently. By analyzing the relationshipbetween resolution and time information of rules, we propose a method to decide timeorders among time-related elements.Whether a rule can be used or not depends on whether its constraint systemis satisfiable or not. Therefore, this thesis investigates the constraint system in thismodel, presents an e?ective algorithm to determine whether the constraint system hasa solution, and prove it is polynomial. Since there are lots of redundant inequalitiesin the constraint system, this thesis considers this problem, and gives abstractiontheory to simplify this system according to its characteristics. This theory can reducecomputation and costs of time and space. 5. Design and implementation of an e?ective security protocol verification tool SPVT-II.This thesis gives the implementation of the algorithms of the prediction for non-termination and the framework of abstraction and refinement. By combining exactverification and abstract verification, we design and implement an e?ective securityprotocol verification tool SPVT-II based on an automatic protocol verification toolSPVT. This tool can report potential counterexamples in protocols with less falseattacks.6. Analysis and verification of Kerberos protocol.This thesis analyzes Kerberos protocol, models the Authentication Service Ex-change of public-key Kerberos protocol, and then, verifies it automatically by SPVT-II. The experiment result shows that SPVT-II can check a man-in-the-middle attackin this protocol.