Introduction A computationally sound prover A computationally sound logic The modular approach Conclusion

Introduction A computationally sound prover A computationally sound logic The modular approach Conclusion FormaCrypt: Formal Computational Cryptography Bruno Blanchet1, David Pointcheval1 Jean Goubault-Larrecq2, Stephanie Delaune2, Steve Kremer2 Veronique Cortier3, Heinrich Hordegen3, Mathieu Turuani3 Eugen Zalinescu3, Martın Abadi4 1LIENS 2LSV 3LORIA 4UCSC & Microsoft Research November 2007 Bruno Blanchet et al FormaCrypt: Formal Computational Cryptography

• modular approach


• security protocols


• computationally sound prover


• participants laboratoire d'informatique de l'ecole normale


• automatic computationally