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.
» Download Paper [PDF, 64KB]
