Mixed Strand Spaces

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