Automatic analyzer for security protocol verification

We propose a new efficient automatic algorithm for security protocol verification. It is based on an improved authentication tests model. which enhances the original authentication tests by introducing the notion of message type and checking mechanism. This automatic algorithm can provide the precise proof of authentication and secrecy properties of security protocols. The improved authentication tests model is an extension of the original authentication tests, which overcomes the deficiency of the original ones in proving symmetric key protocols. By integrating the message type and checking mechanism, it is easy to identify the originator of the uniquely originating value, and detect the message replayed attack. in addition, this automatic algorithm also exploits the forward proving strategy, which only generates limited states during the verification procedure run and avoids the state spaces explosion. When the valuation procedure terminates, it outputs either the whole proving process or the potential flaws in the security protocol.