Communication space reduction for formal verification of secure authentication protocols

As the share of electronic transactions in commerce grows, the role of the authentication protocol becomes more important. However it is yen, important to ensure that no errors exist in these protocols. Formal methods are a good approach to validate the properties of authentication protocols. Among them, model checking is one of the preferred methods since it can be done automatically. Although protocol designers can use model checking to evaluate their protocols, they, cannot verify all the desired properties completely using this approach because the state space of communication systems cannot be limited. It is, therefore, important to develop techniques to reduce the space of proposed protocols so that model checkers can be used to validate theta. We propose a new space reduction method for validating authentication correctness to support model checking, which is simple and provides tight bounds on the state space.