Welcome to the resource topic for
**2003/145**

**Title:**

Symmetric Authentication Within a Simulatable Cryptographic Library

**Authors:**
Michael Backes, Birgit Pfitzmann, 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.

**ePrint:**
https://eprint.iacr.org/2003/145

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

**Example resources include:**
implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .