Campus Event Calendar
Event Entry
What and Who
Analysis of Cryptographic Protocols with Probabilistic Automata
Roberto Segala
Universty of Verona
Virtual Seminar
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 5 December 2008
13:30
60 Minutes
E1 4
019
Saarbrücken
Abstract
We show how the model of probabilistic automata together with its
simulation-based proof techniques can be used for the analysis of
protocols that involve cryptographic primitives. After giving a brief
introduction to the main features of probabilistic automata and
simulation relations, we consider a simple case study to argue that
exact relations are not adequate in general for cryptography, leading to
a new notion of Approximated Computationally Bounded Simulation
Relation, where the step condition holds up to an exponentially small
error provided that computations are of polynomial length. We argue that
in this way it is possible to build rigorous compositional proofs by
showing how the logical negation of the step condition of a symulation
relation becomes the definition of an attacker for the underlying
cryptographic primitives. We conclude with a high level description of
some work in progress aimed at applying the same technique for proving
Dolev-Yao soundness and for proving the correctness of the Crypto
Library of Backes, Pfitzmann and Waidner.
simulation-based proof techniques can be used for the analysis of
protocols that involve cryptographic primitives. After giving a brief
introduction to the main features of probabilistic automata and
simulation relations, we consider a simple case study to argue that
exact relations are not adequate in general for cryptography, leading to
a new notion of Approximated Computationally Bounded Simulation
Relation, where the step condition holds up to an exponentially small
error provided that computations are of polynomial length. We argue that
in this way it is possible to build rigorous compositional proofs by
showing how the logical negation of the step condition of a symulation
relation becomes the definition of an attacker for the underlying
cryptographic primitives. We conclude with a high level description of
some work in progress aimed at applying the same technique for proving
Dolev-Yao soundness and for proving the correctness of the Crypto
Library of Backes, Pfitzmann and Waidner.
Contact
Jennifer Müller
900
--email hidden
Video Broadcast
Yes
passcode not visible
logged in users only
Jennifer Müller, 12/02/2008 12:04
Jennifer Müller, 12/01/2008 16:12 -- Created document.
Jennifer Müller, 12/01/2008 16:12 -- Created document.