Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.
Le séminaire du LSV est public et ne nécessite aucune inscription préalable.
Visiter le site web pour cet événement | Exporter cet événement au format iCalendar
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”.
Exporter l'agenda au format iCalendar | Les séminaires précédents