Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 7 juin, 10h30 ------------------ Benjamin Grégoire ------------------ INRIA ======================================================= Formal certification of code based cryptographic proofs ======================================================= I will present CertiCrypt, a tool built on top of the Coq proof assistant, for checking exact security proofs of cryptographic primitives. After a brief introduction to the notions of exact security and game playing methodology, I will present the key point of CertiCrypt: The Probabilistic Relational Hoare Logic. I will show how the pRHL can be used to justify different program transformations and how those transformations can be used to build automatic tactics in Coq. Then, I will explain how we can reason on unknown adversaries. Finally I will present other techniques developed in CertiCrypt and illustrate the talk with examples.