FORMES seminar, Tue, 26 May 2009 16:00
Title： Models for security protocols
Venue： Tsinghua University, FIT Building, Room 1-415
Speaker： Hubert Comon-Lundh, INRIA Saclay & AIST-Tokyo

There are several approaches to the verification of security protocols. In the
“Dolev-Yao” approach, the attacker is modeled as an inference system
operating on messages. This approach has resulted in several automated
verification tools, as well as theoretical results. In the “computational
security” approach, the intruder is an arbitrary PTIME probabilistic
interactive Turing machine, a model that is far more difficult to work with (
and there is no automated verification tool).
We describe under which assumptions the first model is a faithful abstraction
of the second. As a result, computational security properties become provable
in a formal system using a variety of existing tools.