Research On Two Formal Theories Of Security Protocols

In this dissertation, we discuss some problems related to the two theories of the formal methods in the field of security protocols, and our work is mainly on the formal analysis about three-part authenticated key-exchange protocols.With the advance of the Internet, the efficiency of communications is greatly improved, which bulkily changes appearances of people's methods of living, studying, and working. But at the same time, the problem of information security caused by anonymity and publicity of INTRENET arises people's misgivings.In order to solve the problem of information security, people already designed a lot of security protocols for secure applications. Security protocol are process having two or above participants to complete a kind of security task. It has three points: firstly, protocols have two participants at least. Secondly, participants must deal with messages and exchange messages by turns. Thirdly, protocols must achieve some kind of security task.Elaborately designed messages of protocol have delicate interactive relationship, so if we analyze protocols using non-formal methods, defects are hardly to be found commonly. In order to solve the problem, we need to recur to the method of formal analysis. Formal analysis is a mathematic method used to describe system properties and its purpose is to find ambiguity, congruity, and imperfection of a system. The system may be so big as a enterprise system including software and hardware, or so small as protocols including some messages. Through formal analysis methods, we can disclose messages' inherent meanings, and verify protocols' rightness. If a protocol isn't secure, formal analysis method can find the reason and advance the opinion about mending the protocol.