ARA SSIA Formacrypt

(January 2006 - July 2009)

This project is supported by Agence Nationale de la Recherche (ANR), Action de Recherche Amont Sécurité, Systèmes embarqués et Intelligence Ambiante (ARA SSIA).

Goal

The verification of cryptographic protocols is a very active research area. Most works on this topic use either the computational approach, in which messages are bitstrings, or the formal approach, in which messages are terms. The computational approach is more realistic but more difficult to automate. The goal of our project is to bridge the gap between these two approaches.

Members

Detailed description of the project

A more detailed description of the project is available (application to ARA SSIA, June 2005).

Workshops

Meetings

STIC meetings

Evaluation

Publications

M. Abadi, M. Baudet, and B. Warinschi. Guessing attacks and the computational soundness of static equivalence. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06), Vienna, Austria, March 2006, LNCS 3921, pages 398-412. Springer.

M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and Proofs of Protocol Security: A Progress Report. In 21st International Conference on Computer Aided Verification (CAV'09), volume 5643 of Lecture Notes in Computer Science, pages 35-49, Grenoble, France, June 2009. Springer.

M. Abadi and B. Warinschi. Security Analysis of Cryptographically Controlled Access to XML Documents. Journal of the ACM, 55(2), May 2008.

M. Arapinis, S. Delaune and S. Kremer. From One Session to Many: Dynamic Tags for Security Protocols. In LPAR'08, LNAI 5330, pages 128-142. Springer, 2008.

M. Backes, A. Datta, A. Derek, J. C. Mitchell, and M. Turuani. Compositional Analysis of Contract Signing Protocols. Theoretical Computer Science, 367(1-2):33-56, 2006.

M. Baudet, V. Cortier and S. Delaune. YAPA: A generic tool for computing intruder knowledge. In 20th International Conference on Rewriting Techniques and Applications (RTA'09), Brazilia, Brazil, June 2009. Volume 5595 of Lecture Notes in Computer Science, pages 148-163. Springer, 2009.

M. Baudet. Sécurité des protocoles cryptographiques : aspects logiques et calculatoires. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007.

M. Baudet, V. Cortier and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. Information and Computation, 207(4):496-520, 2009.

B. Blanchet. Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. Habilitation à diriger des recherches, Université Paris-Dauphine, France, November 2008.

B. Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006. Long version available as ePrint Report 2005/401, November 2005; revised February 2006, http://eprint.iacr.org/2005/401.

B. Blanchet. Computationally Sound Mechanized Proofs of Correspondence Assertions. In 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 97-111, Venice, Italy, July 2007. IEEE.

B. Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193-207, October-December 2008. Special issue IEEE Symposium on Security and Privacy 2006.

B. Blanchet and A. Chaudhuri. Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In IEEE Symposium on Security and Privacy, pages 417-431, Oakland, CA, May 2008. IEEE.

B. Blanchet, A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 87-99, Tokyo, Japan, March 2008. ACM.

B. Blanchet, A. D. Jaggard, J. Rao, A. Scedrov, and J.-K. Tsay. Refining Computationally Sound Mechanized Proofs for Kerberos. In Workshop on Formal and Computational Cryptography (FCC 2009), Port Jefferson, NY, July 2009.

B. Blanchet and D. Pointcheval. Automated security proofs with sequences of games. In CRYPTO'06, volume 4117 of Lecture Notes in Computer Science, pages 537-554, Santa Barbara, CA, August 2006. Springer. Long version available as ePrint Report 2006/069, February 2006, http://eprint.iacr.org/2006/069.

E. Bresson, Y. Lakhnech, L. Mazaré, and B. Warinschi. A Generalization of DDH with Applications to Protocol Analysis and Computational Soundness. In Advances in Cryptology (CRYPTO'07), volume 4622 of Lecture Notes in Computer Science, pages 482-499, Santa Barbara, CA, August 2007. Springer.

D. Cadé. From CryptoVerif Specifications to Computationally Secure Implementations of Protocols (Work in Progress). In Workshop on Formal and Computational Cryptography (FCC 2009), Port Jefferson, NY, July 2009.

H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), Alexandria, Virginia, USA, October 2008. ACM Press. (Also presented at FCC'08.)

V. Cortier. Verification techniques for cryptographic protocols (invited talk). International Conference on Rewriting Techniques and Applications (RTA'08), July 15-17, 2008. Hagenberg, Austria.

V. Cortier. Verification of Security Protocols. In Proceedings of the 10th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), Savanah, USA, January 2009. Volume 5403 of Lecture Notes in Computer Science, pages 5-13. Springer, 2009. (Invited tutorial)

V. Cortier, J. Delaitre, and S. Delaune. Safely Composing Security Protocols. In Proceedings of the 27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), New Delhi, India, December 2007, LNCS 4855, pages 352-363. Springer.

V. Cortier and S. Delaune. Safely Composing Security Protocols. Formal Methods in System Design, 34(1):1-36, 2009.

V. Cortier and S. Delaune. Deciding knowledge in security protocols for monoidal equational theories . In Proc. of the 14th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), Yerevan, Armenia, October 2007. Volume 4790 of Lecture Notes in Artificial Intelligence, pages 196-210. Springer, 2007.

V. Cortier and S. Delaune. Deciding knowledge in security protocols for monoidal equational theories. Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'07), Wroclaw, Poland, July 2007. Workshop affiliated to LICS'07 and ICALP'07.

V. Cortier, H. Hördegen, and B. Warinschi. Explicit Randomness is not Necessary when Modeling Probabilistic Encryption. Workshop on Information and Computer Security (ICS 2006), Timisoara, Romania, September 2006.

V. Cortier, S. Kremer, R. Küsters, and B. Warinschi. Computationally Sound Symbolic Secrecy in the Presence of Hash Functions. In N. Garg and S. Arun-Kumar (eds.), Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), Kolkata, India, December 2006. Volume 4337 of Lecture Notes in Computer Science, pages 176-187. Springer.

V. Cortier, R. Küsters, and B. Warinschi. A Cryptographic Model for Branching Time Security Properties - the Case of Contract Signing Protocols. In J. Biskup (ed.), Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07), volume 4734 of Lecture Notes in Computer Science, pages 422-437, Dresden, Germany, September 2007. Springer. (Also presented at FCC'07.)

V. Cortier and E. Zalinescu. Deciding key cycles for security protocols. In Proc. of the 13th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Phnom Penh, Cambodia, November 2006. Volume 4246 of Lecture Notes in Artificial Intelligence, pages 317-331. Springer. (Also presented at FCC'07.)

A. Datta, A. Derek, J. Mitchell, and B. Warinschi. Computationally Sound Compositional Logic for Key Exchange Protocols. In 19th IEEE Computer Security Foundations Workshop -- CSFW'06, pages 321-334, Venice, Italy, July 2006.

A. Datta, A. Derek, J. Mitchell, A. Roy, V. Shmatikov, M. Turuani, and B. Warinschi. Computationally Sound Compositional Logic for Security Protocols. In Véronique Cortier and Steve Kremer, editors, 2nd Workshop on Formal and Computational Cryptography, FCC, Venice, Italy, July 2006.

S. Delaune, S. Kremer and M. D. Ryan. Composition of Password-based Protocols. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), Pittsburgh, PA, USA, June 2008, pages 239-251. IEEE Computer Society Press.

H. Hoerdegen. Vérification des protocoles cryptographiques : Comparaison des modèles symboliques avec une application des résultats - Étude des protocoles récursifs. Thèse de doctorat, Université Henri Poincaré, Nancy, France, November 2007.

S. Kremer. Computational soundness of equational theories (Tutorial). In G. Barthe and C. Fournet (eds.), Revised Selected Papers from the 3rd Symposium on Trustworthy Global Computing (TGC'07), Sophia-Antipolis, France, November 2007, LNCS 4912, pages 363-382. Springer, 2008.

S. Kremer and L. Mazaré. Adaptive Soundness of Static Equivalence. In J. Biskup (ed.), Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07), volume 4734 of Lecture Notes in Computer Science, pages 610-625, Dresden, Germany, September 2007. Springer. (Also presented at FCC'07.)

S. Kremer and L. Mazaré. Computationally Sound Analysis of Protocols using Bilinear Pairings. Journal of Computer Security, 2009. To appear.

L. Mazaré. Computationally Sound Analysis of Protocols using Bilinear Pairings. In Preliminary Proceedings of the 7th International Workshop on Issues in the Theory of Security (WITS'07), Braga, Portugal, March 2007, pages 6-21.

E. Zalinescu. Sécurité des protocoles cryptographiques : décidabilité et résultats de transfert. Thèse de doctorat, Université Henri Poincaré, Nancy, France, December 2007.

Software

CryptoVerif is an automatic protocol verifier sound in the computational model.

Module for the computational proof of protocols in AVISPA.


Page maintained by Bruno Blanchet