Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

French / Français

Cryptographic protocols: formal and computational proofs (48h + 12h TD, 6 ECTS)

Teachers for 2010-2011 :

1. Stéphanie Delaune (12h + 3h TD)
2. Steve Kremer (12h + 3h TD)
3. David Pointcheval (12h + 3h TD)
4. Bruno Blanchet (12h + 3h TD)

Goals of the course

Cryptographic protocols are distributed programs which aim at securing communications and transactions by the means of cryptographic primitives. The design of cryptographic protocols is difficult: numerous errors have been discovered in protocols after their publication. It is therefore particularly important to be able to obtain proofs that protocols are secure.

Two models of the protocols have been considered: the formal model and the computational model. We shall present these two models, the associated proof techniques, and results that relate them. We shall also consider their implementation, by showing an automatic proof tool for each model, and by applying them to the verification of programs that implement cryptographic protocols.

This course will be an opportunity to adapt and use formal tools, such as process calculi, semantics, and logic to the particular case of the study of cryptographic protocols.

Course program

1. Modelling protocols and security properties.

1. Examples of protocols and security properties (informal).
2. Formalization of protocols: computational and symbolic setting.
3. Introduction to the applied pi calculus; formalisation of some protocols in applied pi.
4. Cryptographic primitives and their algebraic properties.
5. Security properties; weak secrecy, strong secrecy, authentication, dictionary attacks, indistinguishability properties.

Exercises: modelling protocols in applied pi, description of some attacks.

2. Proofs of protocols in the symbolic model.

1. Deduction problem: passive case. The problem is PTIME complete for local inference systems.
2. Indecidability of security in the case of an active adversary.
3. Bounded number of sessions. Constraints systems and algorithm for trace properties.
4. Decision algorithms for static equivalence.

Exercises: extensions to some other cryptographic primitives.

3. Links between the computational and symbolic models.

1. Full abstraction for static equivalence: the Abadi-Rogaway theorem.
2. Examples of extensions to other primitives, with other assumptions; adaptive adversary.
3. Statement of the results in the active case: trace mapping and full abstraction of observational equivalence.

Exercises: See [8]: the traps and the limits of the method. Also: examples of computational attacks against protocols proved secure in the symbolic model, showing that the various assumptions are necessary.

4. Proofs in the computational model.

1. Indistinguishability and reachability in the computational model; semantic security, non-malleability, relations.
2. Computational provable security: direct approach; algorithmic assumptions, proofs by reduction, standard techniques (hybrids, folding...)
3. Computational provable security: game-based approach; general methodology, example, interpretation of the results.
4. Security of interactive protocols (ideal functionality); methodology, illustration on authenticated key exchange.

Exercises: reductions between algorithmic assumptions, security notions, simple primitives. Security analysis of primitives.

5. Automation of proofs of protocols

1. In the symbolic model: ProVerif tool
   • Formalization with Horn clauses; the ProVerif tool.
   • Bi-processes and formalization of equivalence properties in ProVerif.
2. In the computational model: CryptoVerif tool
   • Automation of proofs by sequences of games: overview of the method, process calculus used for representing games, game transformations (syntactic transformations and transformations that come from computational assumptions), proof of properties on the final game.
   • Introduction and demonstration of the CryptoVerif tool.

Exercises: Modelling protocols in Horn clauses and use of Proverif on some concrete examples. Experimentation with the CryptoVerif tool.

Languages of the course :

The course material will be in English. The course will a priori be in French.
However, if it is attended by non-French-speaking students and in agreement with all students that attend it, this course can also be in English.

Material :

The slides will be made available online on the course web page.

Prerequisites

No specific prerequisites. We will however rely on the general prerequisites of the MPRI (semantics, logic, typing...).

Related courses

Cryptanalysis (2-12-1): Course 2-12-1 presents the aspect complementary to security proofs, that is, the attacks against cryptographic primitives and security models.

Algorithmic number theory for cryptology (2-12-2), Polynomial systems, formal computation, and applications (2-13-1) and Error correcting codes and applications to cryptography (2-13-2): these 3 courses study the validity of some algorithmic assumptions used in security proofs.

Concurrency (2-3): It is strongly recommended to attend course 2-3, since the formal models presented here are models of concurrency (although different from those of course 2-3).

Bibliography

[1] M. Abadi and B. Blanchet. Analyzing security protocols with secrecy types and logic programs. Journal of the ACM, 52(1):102--­146, Jan. 2005.

[2] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), pages 104--­115, London, United Kingdom, Jan. 2001. ACM Press.

[3] M. Arapinis, S. Delaune, and S. Kremer. From one session to many : Dynamic tags for se- curity protocols. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, pages 128-­142, 2008.

[4] J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In 21st IEEE Computer Security Foundations Symposium (CSF'08), June 2008.

[5] K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In ACM Conference on Computer and Communications Security, pages 459­--468, 2008.

[6] B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pages 140­--154, Oakland, California, May 2006. Extended version available as ePrint Report 2005/401.

[7] B. Blanchet and D. Pointcheval. Automated security proofs with sequences of games. In C. Dwork, editor, Advances in Cryptology ­ CRYPTO 2006, pages 537--­554, Santa Barbara, CA, Aug. 2006.

[8] H. Comon-Lundh. Soundness of abstract cryptography. Lecture notes, Part 1. Available here, 2007.

[9] H. Comon-Lundh, V. Cortier, and E. Zalinescu. Deciding security properties of cryptographic protocols. Application to key cycles. Transaction on Computational Logic, 2009. To appear. A preliminary verion is available here.

[10] C. Fournet and T. Rezk. Cryptographically sound implementations for typed information-flow security. In 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 323­--335, 2008.

[11] D. Pointcheval. Advanced Course on Contemporary Cryptology, chapter Provable Security for Public-Key Schemes, pages 133­--189. Advanced Courses CRM Barcelona. (248 pages).

[12] V. Shoup. Sequences of games : a tool for taming complexity in security proofs. Manuscript. Available here.

Possible lecturers

Previous years

• 2009-2010
• 2008-2009
• 2007-2008

Web page maintained by webmastermprimasteruniv-paris7fr.