Campus Event Calendar
Event Entry
What and Who
Symbolic XOR and Hash Functions – Where Abstract Security Protocol Analysis and Cryptography Lose Synchronization
Prof. Michael Backes
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 16 February 2006
13:00
-- Not specified --
45 - FR 6.2 (E1 3)
016
Saarbrücken
Abstract
Tool-supported proofs of security protocols typically rely on
abstractions from real cryptography by term algebras, so-called
Dolev-Yao models. Recently significant progress was made in proving
that Dolev-Yao models can be sound with respect to actual
cryptographic realizations and security definitions. The strongest
results show this in the sense of reactive simulatability/UC, a notion
that essentially means the preservation of arbitrary security
properties under arbitrary active attacks and in arbitrary protocol
environments, with only small changes to both Dolev-Yao models and
natural implementations.
However, these results are so far restricted to cryptographic systems
like encryption and signatures which essentially only have
constructors and destructors, but no further algebraic
properties. Typical modern tools and complexity results around
Dolev-Yao models also allow more algebraic operations. The first such
operation considered is typically XOR because of its clear structure
and cryptographic usefulness. We show that it is impossible to extend
the strong soundness results to XOR, at least not with remotely the
same generality and naturalness as for the core cryptographic
systems. Along a similar line, we show that it is impossible to extend
the strong reactive simulatability/UC results to usual Dolev-Yao
models of hash functions, which constitute one of the most commonly
used operators in these models.
abstractions from real cryptography by term algebras, so-called
Dolev-Yao models. Recently significant progress was made in proving
that Dolev-Yao models can be sound with respect to actual
cryptographic realizations and security definitions. The strongest
results show this in the sense of reactive simulatability/UC, a notion
that essentially means the preservation of arbitrary security
properties under arbitrary active attacks and in arbitrary protocol
environments, with only small changes to both Dolev-Yao models and
natural implementations.
However, these results are so far restricted to cryptographic systems
like encryption and signatures which essentially only have
constructors and destructors, but no further algebraic
properties. Typical modern tools and complexity results around
Dolev-Yao models also allow more algebraic operations. The first such
operation considered is typically XOR because of its clear structure
and cryptographic usefulness. We show that it is impossible to extend
the strong soundness results to XOR, at least not with remotely the
same generality and naturalness as for the core cryptographic
systems. Along a similar line, we show that it is impossible to extend
the strong reactive simulatability/UC results to usual Dolev-Yao
models of hash functions, which constitute one of the most commonly
used operators in these models.
Contact
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 02/13/2006 13:03
Veronika Weinand, 10/19/2005 13:11
Veronika Weinand, 10/19/2005 13:08 -- Created document.
Veronika Weinand, 10/19/2005 13:11
Veronika Weinand, 10/19/2005 13:08 -- Created document.