Authentication Tests Based on Test Type Matrix

The theory of authentication tests is a powerful tool for analyzing and designing cryptographic protocols. However, it is difficult to apply the theory directly to prove the security goals of the protocols because determining the type of the test (e.g. outgoing, incoming and unsolicited test) is a little complex for computer and deriving the security properties of a test needs more intelligence. Therefore, automatic security protocol analyzer cannot be implemented efficiently based on this theory. To solve this problem, in this paper we propose an authentication test type matrix (ATTM), which makes the identification of the test type very simple and straightforward. Furthermore, we propose and prove a set of security properties associated with each case indicated by the elements in the ATTM, which can be used directly in protocol analysis and design. Using the example of Needham-Schroeder protocol, we demonstrate that ATTM makes automatic security protocol verification and design much easier and more straightforward.