Research On Authentication Methods Of Security Protocols Based On Temporal Logic

Security protocols are protocols based on cryptography, they provide a variety of security services in internet and distributed systems. In recent years, the use of formal methods for analyzing security protocols has been gaining a new tendency.We firstly introduce the equivalency theorem of local formulae on the base of distributed temporal logic, give their proofs, and compare with the equivalency theorem of temporal logic. Then describe the IEEE802.11i protocol using distributed temporal logic, and give event structure model of the IEEE802.11i protocol. The detail proofs of the mutual authentication between the principals of the IEEE 802.11i protocol are given.Secondly, on the base of distributed temporal logic, existential quantifier and universal quantifier is added, distributed compute tree temporal logic is introduced. Then state formulae and path formulae are defined, and the semantics of distributed compute tree temporal logic is given. The equivalency theorem of local state formlae and their proofs are given.Lastly, we describe the multi-party certified email protocol using distributed compute tree temporal logic. This protocol’s event structure model and some fairness axioms are introduced. In the below two cases, have trusted third party participating in and no trusted third party participating in, non-repudiation of the sender and receiver is verified.