Pascal Lafourcade

Presentation and Informations

Security models: proofs, protocols and politics

This unit is one of the common core courses in information systems of the Master Pro 2 Security, Cryptology and information coding. The instructors of this unit are Jean-Louis Roch (jean-louis.roch AT imag.fr), Florent Autreau (florent.autreau AT imag.fr) and myself. Course topics:

Introduction
Indistinguishability
Public Encryption
Symmetric encryption
Security protocols: Symbolic Model and Computational Model
Non-interference Problem
Access Control and Security Policies

A paper about Elgamal by Douglas Stinson.
Slides: How to make a presentation?

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	Comments	Lecture Notes
1	24th September 2009	Introduction and Probability	SET 1	Notes 1 2009
2	24th September 2009	Indistinguishability and Security Notions		Notes 2 2009
3	28th September 2009	Reduction Proofs		Notes 3 2009
4	28th September 2009	Hybrid Argument		Notes 4 2009
5	29th September 2009	Symmetric Encryption		Notes 5 2009
6	5th October 2009	Security of Protocols	SET 2	Notes 6 2009
7	12th October 2009	Passive Intruder		Notes 7 2009
8	12th October 2009	Active Intruder		Notes 8 2009
9	2nd November 2009	Tools and Application	SET Tools	Notes 9 2009
10	12th November 2009	Access Control		Notes 10 2009
11	12th November 2009	Non Interference and Others		Notes 11 2009
12	16th November 2009	Link Between Computational and Symbolic	SET 3	Notes 12 2009

3 exercices sessions are planned

1st October 2009
9th November
16th November

Exam 3th December 2009
Mid-unit exam 22th October 2009

Slides of the other lectures will be available as soon as possible.
Notes are written by students and reflect how they follow the lecture, they are not always complete.

LINK TO AVISPA-1.0 Tools used: AVISPA, Hermes, Proverif, Scyther, Xor and DH Proverif.

Material for practice session in Computer Room: protocol1.spdl, protocol2.spdl, needham.horn.

Scripts: install-verif-tools08-09.sh PATH variable useful for the Computer exercices session:
export PATH=$PATH:.:$HOME/VeriTools/scyther
export PATH=$PATH:.:$HOME/VeriTools/proverif1.15
export AVISPA_PACKAGE=$HOME/VeriTools/avispa-1.0
export PATH=$PATH:$AVISPA_PACKAGE

Lectures Notes

Empty.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_08_XX.tex

Lecture 1, 24th September 2009 scribes are: LEFERVRE Antoine, LINGE yanis, BEQUIDT Benoit
Lecture 2, 24th September 2009 scribes are: CARON Julien, HABRAKER Remi, STORDEUR Jeremie
Lecture 3, 28th September 2009 scribes are: GABIAM Amanda, ARNEDO Pedro, ROUAULT Boris
Lecture 4, 28th September 2009 scribes are: TERRADE Vanessa, MEFFRAY guillaume, BARJON anthony
Lecture 5, 29th September 2009 scribes are: ROJAT Antoine, MANGEOT Guillaume, THARAND Jeremie
Lecture 6, 5th October 2009 scribes are: ALAWADI, ALNOON, ALTAMIMI
Lecture 7, 12th October 2009 scribes are: LU Wei, Frederic Mejean, COGNEE Partice, PILLARD
Lecture 8, 12th October 2009 scribes are: KOLOKOSO Daniel, ALALI, AL Mansoori, BANI Hasshim
Lecture 9, 2nd November 2008 scribes are: RIPERT Loic, WLOKA Stéphane, JAVELLE Jerome
Lecture 10, 12th November 2008 scribes are: NJIA Marvin, VANGJEL Endri
Lecture 11, 12th November 2008 scribes are: DUCLOS Mathilde, DEVILLEZ Florian, JUILLARD Violaine
Lecture 12, 16th November 2008 scribes are: Shamise,Ypusuf, Raeisi, K. Mohamed, Mohamed Naiumi

Online References

Introduction to Probability by Charles M. Grinstead and J. Laurie Snell. 520 pages.
A Computational Introduction to Number Theory and Algebra by Victor Shoup. 517 pages.

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.
Reference card for Emacs.

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

Articles in Security to read by group

5 students max per article, due to constraints you have only 9 possibilities of articles Presentation will be 27th November Morning 8.00 am .

8.00 - 8.20 Relations Among Notions of Security for Public-Key Encryption Schemes Crypto'98 by Mihir Bellare, Anand Desai, David Pointcheval and Phillip Rogaway
STUDENTS: Terrade Vanessa, Barjon Anthony, Meffray Guillaume, Eisa Al Shamsi, Khuloud Mohamed PAPER FULL. ABSTRACT
8.30 - 9.00 Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption) 2000, by Martín Abadi, Phillip Rogaway in IFIP International Conference on Theoretical Computer Science (IFIP TCS2000)
STUDENTS: Violaine Juillard, Wloka Stéphane, Jérome JAVELLE, Guillaume MANGEOT, Loic Ripert FULL PAPER . ABSTRACT SLIDES
9.00 - 9.30 Cas Cremers Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement In CCS '08: Proceedings of the 15th ACM conference on Computer and communications security, Alexandria, Virginia, USA.
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols In Computer Aided Verification: Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), Princeton, USA, 2008.
STUDENTS: Shaima Al Awadi / Hassan Alnoon / Sultan Altamimi / Omar Bani Hasim, Antoine ROJAT FULL PAPER ABSTRACT SLIDES
9.30 - 10.00 Bruno 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. Electronic version available at http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.
STUDENTS: Patrice Cognee, Daniel Kolokosso, Jeremie THARAUD, Loic PILLARD, Frédéric Méjean ABSTRACT SLIDES
10.30 - 11.00 OAEP Reconsidered (2000) by Victor Shoup
STUDENTS: Pedro Arnedo, ROUAULT Boris, Remi Habraken, Linge Yanis, Amanda Gabiam. PAPER FULL. ABSTRACT
11.00 - 11.30 A Sound Type System For Secure Flow Analysis (1996) by Dennis Volpano , Geoffrey Smith , Cynthia Irvine
STUDENTS: Endri Vangjel, Marvin TCHOULA NJIA, Mohamed AL ALI , Mohamed AL MANSOORI FULL PAPER. ABSTRACT SLIDES
11.30 - 12.00 M. Bellare, A. Desai, E. Jokipii and P. Rogaway. A Concrete Security Treatment of Symmetric Encryption: Analysis of the DES Modes of Operation. The preliminary version of this paper was entitled A Concrete Security Treatment of Symmetric Encryption and appeared in the Proceedings of 38th Annual Symposium on Foundations of Computer Science, IEEE, 1997.
STUDENTS : Duclos Mathilde, Floran Devillez, yousuf alboloushi, mohamed Alnuaimi, Hamad RAEISI FULL PAPER ABSTRACT SLIDES
Later. David Basin, Sebastian Moedersheim, and Luca Viganò. OFMC: A symbolic model checker for security protocols. In International Journal of Information Security, 4 (3), pages 181-208, 2005.
Sebastian Moedersheim and Luca Viganò. The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols. Fosad 2007-2008-2009, LNCS 5705, 166-194. Springer-Verlag, 2009.
STUDENTS: Caron, Stordeur, Dequidt, Lefebvre ABSTRACT

Articles in Security

Relations Among Notions of Security for Public-Key Encryption Schemes Crypto'98 by Mihir Bellare, Anand Desai, David Pointcheval and Phillip Rogaway
Sequences of Games: A Tool for Taming Complexity in Security Proofs, 2004, by Victor Shoup.
On the Security Notions for Public-Key Encryption Schemes SCN '04, by Duong Hieu Phan and David Pointcheval.
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption) 2000, by Martín Abadi, Phillip Rogaway in IFIP International Conference on Theoretical Computer Science (IFIP TCS2000)
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 Juergen 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.
French lecture notes by Véronique Cortier.