Many security protocols have the aim of authenticating one agent acting as initiator to another agent acting as responder and vice versa. Sometimes, the authentication fails because of executing several parallel sessions of a protocol, and because an agent may play both the initiator and responder role in parallel sessions. We take advantage of the notion of transition systems to specify authentication for parallel multiple sessions execution. To model the authentication, two main notions called 1. agent's scope and 2. agent's recognizability are introduced, which consider the difference of ability of agents due to their different roles in the protocol and different access to keys and secrets. To formalize above notions, a process algebra provided by some primitives for manipulating cryptographic messages is used. We formalize some security protocols and examine our definition of authentication for them. We just discuss the symmetric key case.

Keywords