Next Loria Security Seminar will take place on Tuesday, 10th June at 1pm in room B011-B013.

Guillaume Scerri (ENS Paris-Saclay, LMF), will give a presentation entitled Capturing new cryptographic proofs techniques using logic: extension to the computationally complete symbolic attacker.

When proving cryptographic protocols, one has to deal with a malicious attacker. In particular this means that it is crucial to carefully capture attacker capabilities. This is best done by reducing security of protocols to known hard problems. However these cryptographic reductions can be quite complex and when done by hand such reductions can be rather hard to check. In recent years there has been a push to capture such reductions using logics that can be checked using (dedicated) proof assistants. In this talk we explore the intricacies of capturing complex cryptographic reductions in one of these logics the Computationally Complete Symbolic Attacker logic. We will focus on two main techniques: hybrid arguments and rewinding, and show how they can be applied to proofs of new protocols, namely e-voting mixnets.