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