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 very 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 the proposed protocols so that model checkers can be used to validate them. 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