Improvements of authentication tests on detecting type flaw attacks

Authentication tests are widely used in formal analysis, design and automatic verification of security protocols. However, they are not sufficient in proving symmetric key protocols, and fail to detect potential attacks on Neuman-Stubblebine protocol. By analyzing the failure reasons of authentication tests, some of their deficiencies have been pointed out. In order to break through these limitations of analytic capability of the original authentication tests, the improved authentication tests (I-ATs) have been proposed. In the I-ATs, the notion of message type is introduced for detecting the possibility of certain replay and interleaving attacks. The proofs of Neuman-Stubblebine protocol and Kao-Chow authentication protocol show that the I-ATs can easily find the type flaw attack on the initial authentication of Neuman-Stubblebine protocol, and give precise proof for Kao-Chow protocol.