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

Coordonnées

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 and needham.pi

PATH variable useful for the Computer exercices session:

export AVISPA_PACKAGE=/opt/avispa/

export PATH=$PATH:$AVISPA_PACKAGE

- 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.

- 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.*

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.

- Two volumes of: The Foundations of Cryptography by Oded Goldreich
- Bruce Schneier, Applied cryptography,
- Matt Bishop, Computer Security: Art and Science,
- Douglas Stinson, Cryptography: Theory and Practice,
- Simon Singh, The Code Book: The Secret History of Codes and Code Breaking.
- Christos Papadimitriou, Computational Complexity, Edition Addison Wesley, 1994.