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 preplay 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.