Pascal Lafourcade

Presentation and Informations

Models and analysis of security protocols:

We introduce symbolic and automatic verification of cryptographic protocols using different techniques. We illustrate the theoritical results by various concret examples of protocols, showing each time existing flaws. Course topics for the first Part:

Introduction
Dolev Yao Model
Locality Result
Constraints, Resolution
Impossibility Result
Applications with Tools

Second part is about Logic and Automata. You have all material for the second part here.

Coordonnées

Adresse

Pascal Lafourcade
Laboratoire Verimag centre Equation
2, avenue de Vignate
38610 Gières
FRANCE

Bureau	:	CTL1/B4D
Tél	:	+33 (0) 4 56 52 04 14
Mobile	:	+33 (0) 6 83 54 90 70
Fax	:	+33 (0) 4 56 52 03 44
E-mail	:	pascal.lafourcade@imag.fr

Verimag Webmail

Material

Number	Date	Lecture	Exercises	Comments	Lecture Notes
1	11th October 2007	Introduction	Set 1		Notes 1
2	18th October 2007	Dolev Yao	Set 2	Corrected
3	25th October 2007	Active Intruder	Set 3	Corrected
4	8th November 2007	Tools	Set 4	READY

Slides of the other lectures will be available as soon as possible.

Tools used: AVISPA, Hermes, Proverif, Scyther.
Material for practice session in Computer Room: protocol1.spdl, protocol2.spdl, needham.horn.

PATH variable useful for the Computer exercices session:
export PATH=\$PATH:/opt/ach/lafourcade/SCYTHER/scyther
export PATH=\$PATH:/opt/ach/lafourcade/PROVERIF/proverif1.14pl2/
export AVISPA_PACKAGE=/opt/ach/lafourcade/AVISPA/avispa-1.0
export PATH=\$PATH:\$AVISPA_PACKAGE

Lectures Notes

Empty_M2R.tex is a LaTex file that you have to use for the notes of the lecture to have some uniformity.
PLEASE NAME YOUR FILE : Lecture_Note_XX.tex

11th October 2007 scribe is: Marion Daubignard
18th October 2007 scribe is:
25th October 2007 scribe is:
8th November 2007 scribe is:

References for LaTex

List of useful material to use LaTex

Essential LaTeX ++ by Jon Warbrick, David Carlisle, Michel Goossens, Sebastian Rahtz, and Adrian Clark. 27 pages.
The Not So Short Introduction to LaTeX2e by Tobias Oetiker, Hubert Partl, Irene Hyna, Elisabeth Schlegl. 101 pages
A simplified introduction to LaTex, in english. 140 pages, well writen many details and examples.
List of math symbols in LaTeX. Only 6 pages of basics LaTex symbols in mathematics. Indispensable.
Complete list of symbols , by Scott Pakin. Very indispensable.
Small Introdutcion to LaTex by Nicolas Markey in French. 60 pages well written for simple and nice things.
Joli manuel pour LaTeX by Benjamin Bayart in French. 150 pages with many details and very usefull.

If you use Linux please use Ispell to avoid typos in your file.

Articles in Security

Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption) 2000, by Martin Abadi, Phillip Rogaway in IFIP International Conference on Theoretical Computer Science (IFIP TCS2000)
An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, by Bruno Blanchet. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.
Verification of Cryptographic Protocols: Tagging Enforces Termination, by Bruno Blanchet and Andreas Podelski. Theoretical Computer Science, 333(1-2):67-90, March 2005. Special issue FoSSaCS'03.
Protocol insecurity with finite number of sessions is NP-complete. M. Rusinowitch and M. Turuani. In Proc. 14th IEEE Computer Security Foundations Workshop, pages 174-190, 2001.
Constraint solving for bounded process cryptographic protocol analysis. J. Millen and V. Shmatikov. In Proc. 8th ACM Conference on Computer and Communications Security (CCS'01), pages 166-175, 2001.
Automatic recognition of tractability in inference relations. D. McAllester. Journal ACM, 40(2):284-303, 1993.
On the security of public key protocols. D. Dolev and A. Yao. IEEE Transactions on Information Theory, 29(2):198\u2013 208, 1983.
Undecidability of bounded security protocols. N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. In Proc. Workshop on formal methods in security protocols, Trento, Italy, 1999.
Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or. S. Delaune, P. Lafourcade, D. Lugiez and R. Treinen. In Michele Buglesi, Bart Preneel, Vladimiro Sassone and Ingo Wegener (eds.), Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06) - Part II, Venice, Italy, July 2006, Lecture Notes in Computer Science 4052, pages 132-143. Springer.
Intruder Deduction for the Equational Theory of Abelian Groups with Distributive Encryption. P. Lafourcade, D. Lugiez and R. Treinen. Information and Computation 205(4), pages 581-623, 2007. Intruder Deduction for AC-like Equational Theories with Homomorphisms. P. Lafourcade, D. Lugiez and R. Treinen. In Jürgen Giesl (ed.), Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05), Nara, Japan, April 2005, Lecture Notes in Computer Science 3467, pages 308-322. Springer.