Formal Methods For Security Protocol Analysis And It's Application

Protocol is a group of rules and promises that two principals or multi-principals exchange messages each other in the computer network and a distributing system. A security protocol is this kind protocol that, by meaning of encrypts and decrypts, hides or obtains message in order to achieve all security aims. In 1970's formal methods for security protocol analysis came forth. Now formal methods for security protocol analysis have become a hotspot domain, and a lot of methods of formal methods and logic well up.Strand Space Model (SSM) is a formal method combining with theorem proving and model checking. In facts SSM is a practical, intuitive and strict formal method for security protocol analysis. With SSM someone has developed an automatic verification tool, ATHENA, which is able to prove the correctness of some authentic and secret protocols, suffered from seriously state space explosion problem and do an imperfect work on secret protocols. Combining with theorem proving and model checking, we developed a new efficient automatic verification algorithm, AVSP. It is the first one that uses the concept of honest ideal to define secrecy of protocol and the first one that utilizes honest ideal logic to specify secrecy property. We also develop pruning methods of the state space in it the results got by verifier of the weaker non-injective agreement of the Needham-Schroeder protocol。It shows that these pruning methods can perfectly reduce state search space and prevent state explosion. The analysis of experimental results shows that AVSP is right and efficient.