## Cryptology ePrint Archive: Report 2003/145

**Symmetric Authentication Within a Simulatable Cryptographic Library**

*Michael Backes and Birgit Pfitzmann and Michael Waidner*

**Abstract: **Proofs of security protocols typically employ simple abstractions of
cryptographic operations, so that large parts of such proofs are
independent of cryptographic details. The typical abstraction is
the Dolev-Yao model, which treats cryptographic operations as a
specific term algebra. However, there is no cryptographic semantics,
i.e., no theorem that says what a proof with the Dolev-Yao
abstraction implies for the real protocol, even if provably secure
cryptographic primitives are used.

Recently we introduced an extension to the Dolev-Yao model for which
such a cryptographic semantics exists, i.e., where security is
preserved if the abstractions are instantiated with provably secure
cryptographic primitives. Only asymmetric operations (digital
signatures and public-key encryption) are considered so far. Here we
extend this model to include a first symmetric primitive,
message authentication, and prove that the extended model still has
all desired properties. The proof is a combination of a probabilistic,
imperfect bisimulation with cryptographic reductions and static
information-flow analysis.

Considering symmetric primitives adds a major complication to the
original model: we must deal with the exchange of secret keys, which
might happen any time before or after the keys have been used for
the first time. Without symmetric primitives only public keys need
to be exchanged.

**Category / Keywords: **foundations / cryptographic protocols, security analysis of protocols, symmetric authentication, cryptographically composable operators

**Publication Info: **Esorics 2003

**Date: **received 25 Jul 2003

**Contact author: **mbc at zurich ibm com

**Available format(s): **Postscript (PS) | Compressed Postscript (PS.GZ) | BibTeX Citation

**Version: **20030725:202252 (All versions of this report)

**Discussion forum: **Show discussion | Start new discussion

[ Cryptology ePrint archive ]