Sciweavers

Share
ESORICS
2004
Springer

A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol

12 years 1 months ago
A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol
We present the first cryptographically sound security proof of the well-known Otway-Rees protocol. More precisely, we show that the protocol is secure against arbitrary active attacks including concurrent protocol runs if it is implemented using provably secure cryptographic primitives. Although we achieve security under cryptographic definitions, our proof does not have to deal with probabilistic aspects of cryptography and is hence in the scope of current proof tools. The reason is that we exploit a recently proposed ideal cryptographic library, which has a provably secure cryptographic implementation. Together with composition and preservation theorems of the underlying model, this allows us to perform the actual proof effort in a deterministic setting corresponding to a slightly extended Dolev-Yao model. Besides establishing the cryptographic security of the Otway-Rees protocol, our result also exemplifies the potential of this cryptographic library. We hope that it paves the wa...
Michael Backes
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where ESORICS
Authors Michael Backes
Comments (0)
books