C.J.F. Cremers, S. Mauw and E.P. de Vink
Injective synchronisation: An extension of the authentication hierarchy

Authentication is one of the foremost goals of many security
protocols. It is most often formalised as a form of agreement, which
expresses that the communicating partners agree on the values of a
number of variables. In this paper we formalise and study an
intensional form of authentication which we call
synchronisation. Synchronisation expresses that the messages are
transmitted exactly as prescribed by the protocol description.
Synchronisation is a strictly stronger property than agreement for the
standard intruder model, because it can be used to detect pre-play
attacks. In order to prevent replay attacks on simple protocols, we
also define injective synchronisation. Given a synchronising protocol,
we show that a sufficient syntactic criterion exists that guarantees
that the protocol is injective as well.