Key Compromise, Strand Spaces, and the Authentication Tests1 1I gave my MFPS 17 talk on 24 May 2001, Bob Dylan's sixtieth birthday. This paper is dedicated to him.
Joshua D. Guttman · Electronic Notes in Theoretical Computer Science · 2001
Some cryptographic protocols are vulnerable to replay attacks, a type of weakness that was a focus of attention in the Burroughs-Abadi-Needham logic. Newer, more operational approaches to protocol analysis have not concentrated on this type of attack. This paper fills the gap for the strand space theory. The main technical point is to provide a definition of recency. Our candidate is convenient because we already have a powerful way to prove events recent, namely the incoming and outgoing authentication tests. A secondary purpose of this paper is to illustrate an easily mechanized pattern for using the authentication tests.