Automatic Verifying Security Protocols Basing Term Guessing And Hash Forging

The security protocols provide security services for the network information exchange and are the foundation of the network security. However the intruder can implement various attacks using flaws of security protocols'own. Whether the security protocols are safe becomes the most critical problem. Earlier analyzing by artificial proving is extremely fallible. The examination scope is also too narrow. It is urgent to design more believable formalize analysis methods.This paper proposes the validating logic for formlly analyzing security protocols.This method has improvements about two important aspects: formalizing protocols and designing intruder model. It effectively overcomes the flows of logical proof method basing on the belief, and it can not only find the attack, but also prove the security of protocols. This paper also proposes a kind of expansion intruder model with applying the theories about term guessing and Hash collisions. Term guessing is the new hot spot in protocol analysis research recent years.Hash collision is the up-to-date significant breakthrough about cryptology basing on which we propose Hash-forge for the first time.Due to these expansions our method has found more attacks. This paper gives some useful comments about how to effectively avoid these new kinds of attacks.Furthermore this paper analyzes two important kind of protocols——e-commerce protocol and the security socket level protocol.At the end, we implement a security protocols automatically analysis system basing on the validating logic and intruder model proposed, and design a protocol specification language.We first time propose the design thought that classificating the specification language while implementing. Comparing with current tools, our system can analyze more types, find more flow and prove more credibly.According the result we searched, the guessing attack of Woo-LamΠ4 and the Hash forge attack of MS-CHAPv2 have never found before.Our research is referrence for the verifying and designing of security protocols, even for the security of the netwok for military, electronic commerce and wireless communications.