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.
Despite using very coarse abstractions, and making strong assumptions on
the environment, the symbolic analysis of cryptographic protocols has
proven very successful. By now, many dimensions of the symbolic
(Dolev-Yao) model have been explored to some extent, including
compositionality properties of protocols and the relation between
symbolic correctness proofs and computational proofs.
One might expect that formal approaches are ideally suited for building larger communication infrastructures, because of their high level of abstraction. However, in practice, symbolic methods are only used for analysis of existing protocols, whereas protocol construction is performed at the detailed level of cryptographic protocols.
In this talk we cover some of the requirements for using cryptographic protocols as components in symbolic, Dolev-Yao like, analyses. In particular, we discuss various compositionality results, and their relation to using cryptographic protocols as building blocks. Finally, we revisit the cryptographic requirements on real-world protocols and show how they influence the compositionality problem, and conclude with a number of open problems.