The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
In this talk we will show how it is possible to use Probabilistic Automata for the verification of security protocols, and in particular how simulation-based proofs can be employed. The simulation method is useful in general to reduce the analysis of global properties to the analysis of local properties of single computational steps. We extend the same idea to analyze global security properties. Since security holds under computational assumptions and up to a negligible probability of error, we propose a notion of polynomially accurate simulation relation for Probabilistic Automata and we illustrate it by analyzing a simple authentication protocol. In particular we show how the negation of the step condition of our simulation relation becomes the definition of a forger for a signature scheme.