Verifying Untimed Version of the WMF Protocol Using networks of Autamata

In this paper we present some results of symbolic verification of untimed version of The Wide-Mouth Frog Protocol. This protocol is designed for achieving authentication between communicating sides in the computer network and exchange a new session cryptographic key. For our investigation we model executions of this protocol by a network of synchronized untimed automata. We investigate suitable protocols properties by testing reachablity of some distinguished states in the defined network. We use VerICS [5] - the symbolic model checker - for searching in our network.