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.
Type systems, relational logics, and interactive proof assistants are effective tools for verifying the security of programs and systems that rely on cryptography. They can provide automation, modularity and scalability. As illustrated in recent case studies, they can be usefully applied to large security protocols and applications [Bhargavan et al., 2008, Fournet et al., 2009].
However, their models traditionally rely on abstract assumptions on the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions in lower-level models that precisely account for the complexity and probability of attacks. These models are more complex and realistic, but recent results suggest thay they are also amenable to formal automated verification [Blanchet, 2006, Barthe et al., 2009, Acar et al., 2011].
I will present our on-going work in adapting and extending our programming and verification framework based on refinement types for ML programs [Bengtson et al., 2008, Bhargavan et al., 2010, Fournet, 2011] which currently uses a combination of automated proofs (using Z3, an SMT solver) and interactive proofs (using Coq), in order to produce machine-checked security proofs of cryptographic programs and libraries under concrete computational assumptions.
This work is part of the “Secure Distributed Computations” group of the “MSR-INRIA Joint Centre”.