Automatic validation of secure authentication protocols.

摘要

With the growing role of e-commerce in commercial transactions, the role of secure authentication protocols has become increasingly more important. Ironically, authentication protocols have been prone to design errors and many authentication protocols are shown to be vulnerable to attacks. It is, therefore, important to develop methods for ensuring that security protocols have minimal vulnerabilities.; Many techniques have been proposed for validating the correctness of security protocols. Among these, general purpose model checking is one of the preferred methods, since it can be performed automatically. Therefore, protocol designers can use model checking even if they are not proficient in formal techniques. Although an attractive approach, state space explosion prohibits model checkers from validating secure protocols with a significant number of communicating participants.; In this work, we propose new methods to address the problem of state space explosion. Model checking with pre-configuration is a “divide-and-conquer” approach that reduces the amount of memory required for verification. In the pre-configuration technique, the values of some or all of the protocol variables are pre-determined before running the model checker. As a result, the state space is divided by the preset values. The soundness of the proposed method was proven by showing that the state space of the model checking with pre-configuration is equivalent to that of traditional model checking. Several pre-configurations using different state variables to divide the state space are proposed and the performance of this method is demonstrated by checking the Needham-Schroeder-Lowe Public-Key protocol using an existing model checker. The memory size required for this verification is reduced significantly using the pre-configuration technique, therefore larger designs can be verified than with traditional model checking. Verification time is also reduced since the method permits symmetry to be used more effectively during the model checking.; Message Availability Checking (MAC) is also proposed as a new automatic verification method for authentication protocols. Though model checking with pre-configuration is effective in reducing the memory size and run time required, that method still suffers from explosion problems in space and time. With implicit message exchanges between participants, MAC does not suffer from the problem of explosion in memory size. Moreover, MAC generates verification results that are a hundred to a thousand times faster than the best results of model checking with pre-configuration for the verification of the Needham-Schroeder-Lowe Public-Key protocol.