One protocol (called the primary protocol) is independent of other
protocols (jointly called the secondary protocol) if the question whether
the primary protocol achieves a security goal never depends on whether
the secondary protocol is in use.
In this paper, we use multiprotocol strand spaces ([27], cf. [28])
to prove that two cryptographic protocols are independent if they use
encryption in non-overlapping ways. This theorem (Proposition 7.2) applies
even if the protocols share public key certificates and secret key "tickets".
We use the method of [8, 7] to study penetrator paths, namely sequences
of penetrator actions connecting regular nodes (message transmissions
or receptions) in the two protocols. Of special interest are inbound
linking paths,which lead from a message transmission in the secondary
protocol to a message reception in the primary protocol. We show that
bundles can be modified to remove all inbound linking paths, if encryption
does not overlap in the two protocols. The resulting bundle does not
depend on any activity of the secondary protocol. We illustrate this
method using the Neuman-Stubblebine protocol as an example [21, 27].
» Download Paper [PDF, 64KB]
