Defining authentication in a trace model
Cas J. F. Cremers, Sjouke Mauw, de E.P. Vink · 2003
Abstract. In this paper we define a general trace model for security protocols which allows to reason about various formal definitions of au-thentication. In the model, we define a strong form of authentication which we call synchronization. We present both an injective and a non-injective version. We relate synchronization to a formulation of agree-ment in our trace model and contribute to the discussion on intensional vs. extensional specifications. 1