Completeness of the authentication tests

Abstract

Protocol participants manipulate values, transforming the cryptographic contexts in which they occur. The rules of the protocol determine which transformations are permitted. We formalize these transformations, obtaining new versions of the two authentication tests from earlier strand space papers. We prove that the new versions are complete, in this sense: any collection of behaviors that satisfies those two authentication tests, when combined with some feasible adversary behavior, yields a possible execution. We illustrate the strengthened authentication tests with brief analyses of three protocols. © Springer-Verlag Berlin Heidelberg 2007.