cette semaine,le jeudi 3 Nov, nous accueillerons
Pierre-Yves Strub (MSR INRIA)
qui donnera un exposé sur
Toward Machine-Checked Program Verification for Concrete Cryptography
L'exposé débutera à 11H en salle 1D23 et sera précédé par un pot informel pour nous retrouver autour de thé, café et croissant: vous êtes les bienvenus à partir de 10H45.
Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.
Amicalement,
Claudia
-----------------------------------------------------------------
Pierre-Yves Strub (MSR INRIA)
Toward Machine-Checked Program Verification for Concrete Cryptography
Jeudi 3 Novembre 2011, 11h salle 1D23
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.
