About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Int. J. Inf. Secur.
Paper
Symmetric authentication in a simulatable Dolev-Yao-style cryptographic library
Abstract
Tool-supported proofs of security protocols typically rely on abstractions from real cryptography by term algebras, so-called Dolev-Yao models. However, until recently it was not known whether a Dolev-Yao model could be implemented with real cryptography in a provably secure way under active attacks. For public-key encryption and signatures, this was recently shown, if one accepts a few additions to a typical Dolev-Yao model such as an operation that returns the length of a term. Here we extend this Dolev-Yao-style model, its realization, and the security proof to include a first symmetric primitive message authentication. This adds a major complication: we must deal with the exchange of secret keys. For symmetric authentication, we can allow this at any time, before or after the keys are first used for authentication, while working only with standard cryptographic assumptions. © Springer-Verlag 2004.