Pascal Lafourcade

Material

Number	Date	Lecture	Comments	C, TD, TP
1	7th November 2011	Introduction : Security Notions	SET 1	C1
2	7th November 2011	Reduction proofs		C2
3	8th November 2011	Public encryption, Reduction Proofs		TD1
4	8th November 2011	Hybrid Argument		TD2
5	8th November 2011	Protocols		C3
6	9th November 2011	Tools	SET 2	C4
7	9th November 2011	Cryptoverif	SET Cryptoverif	TP1 Fichiers
8	9th November 2011	Verification Tools and Applications	SET Tools	TP2
9	10th November 2011	Passive Intruder		C5
10	10 th November 2011	Active Intruder		C6
11	14th November 2011	Formalisation		TD3
12	15th November 2011	Acces Control and Non Interference		C7
13	16th November 2011	Acces Control		TD4
14	16th November 2011	Others		C8
15	18th November 2011	Project		TP3
16	18th November 2011	Project		TP4

LINK TO AVISPA-1.0 LINK TO AVISPA-1.1 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-tools10-11.sh
PATH variable useful for the Computer exercices session:
export PATH=$PATH:$PWD/VeriTools/proverif1.84pl2/
export PATH=$PATH:$PWD/VeriTools/scyther-linux-v1.0-beta9/
export AVISPA_PACKAGE=$PWD/VeriTools/avispa-1.1/
export PATH=$PATH:$AVISPA_PACKAGE

Online References

• Introduction to Probability by Charles M. Grinstead and J. Laurie Snell. 520 pages.
• For background on cryptography, online book: The handbook of applied cryptography by Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone.
• Bellare Rogaway online book Introduction to modern cryptography
• A Computational Introduction to Number Theory and Algebra by Victor Shoup. 517 pages.

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.