| Abstract | Strand space analysis [13, 12] is a method for stating
and proving correctness properties for cryptographic protocols. In this paper we apply the same method to the related problem of mixed protocols, and show that a protocol can remain correct even when used in combination with a range of other protocols.
We illustrate the method with the familiar Otway-Rees [10, 1] protocol. We identify a simple and easily verified characteristic of protocols, and show that the Otway-Rees protocol remains correct even when used in combination with other protocols that have this characteristic.
We also illustrate this method on the Neuman-Stubblebine protocol [9]. This protocol has two parts, an authentication protocol (I) in which a key distribution center creates and distributes a Kerberos-like key, and a re-authentication protocol (II) in which a client resubmits a ticket containing that key. The re-authentication protocol II is known to be flawed [2]. We show that in the presence of protocol II, there are also attacks against protocol I. We then define a variant of protocol II, and prove an authentication property of I that holds even in combination with the modified II. |
