Verification of Cryptographic Protocols

Slides

• 20.10.03: PS, PDF
• 27.10.03: PS, PDF
• 03.11.03: PS, PDF
• 10.11.03: PS, PDF
• 24.11.03: PS, PDF
• 01.12.03: PS, PDF
• 08.12.03: PS, PDF
• 15.12.03: PS, PDF

Exercises

• 21.10.03: PS, PDF
• 28.10.03: PS, PDF
• 04.11.03: PS, PDF
• 11.11.03: PS, PDF
• 25.11.03: PS, PDF
• 02.12.03: PS, PDF
• 09.12.03: PS, PDF
• 16.12.03: PS, PDF

Bibliography

• John Clark and Jeremy Jacob. A Survey of Authentication Protocol Literature. http://www.cs.york.ac.uk/~jac/papers/drareviewps.ps, 1997.

• Bruce Schneier. Applied Cryptography Second Edition: protocols, algorithms, and source code in C. John Wiley & Sons, Inc., 1996.

• Shafi Goldwasser and Mihir Bellare. Lecture Notes on Cryptography. http://www-cse.ucsd.edu/~mihir/papers/gb.ps.gz

• H. Comon-Lundh and V. Cortier. Security properties: two agents are sufficient. In Proc. 12th European Symposium on Programming (ESOP'2003), Warsaw, Poland, Apr. 2003, volume 2618 of Lecture Notes in Computer Science, pages 99-113. Springer, 2003.

• V. Cortier. Vérification automatique des protocoles cryptographiques. (In French.) PhD Thesis, ENS Cachan, March 2003.

• David A. McAllester. Automatic recognition of tractability in inference relations. Journal of the ACM, vol.40, no.2, April 1993.

• E. M. Clarke, S. Jha, and W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET), 1998.

• Nancy A. Durgin, Patrick Lincoln, John Mitchell, et Andre Scedrov. Undecidability of bounded security protocols. Workshop on Formal Methods and Security Protocols (FMSP'99), Trento, Italy, July 5, 1999.

• N.A Durgin, P.D. Lincoln, J.C.Mitchell, A. Scedrov. Multiset Rewriting and the Complexity of Bounded Security Protocols

• M. Rusinowitch and M. Turuany. Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete

• H. Comon-Lundh and R. Treinen. Easy intruder deductions. Research Report LSV-03-8, LSV, ENS Cachan, France, April 2003.

• Martin Abadi and Andrew D. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. SRC Research Report 149, January 25, 1998 110 pages.

• Hubert Comon et Max Dauchet et Rémi Gilleron et Denis Lugiez et Sophie Tison et Marc Tommasi. Tree Automata Techniques and Applications.

• Kumar Neeraj Verma. Automates d'arbres bidirectionnels modulo théories équationnelles (Two-Way Equational Tree Automata). PhD Thesis, ENS Cachan, September 2003.

• Kumar Neeraj Verma. Two-way equational tree automata for AC-like theories: Decidability and closure properties. In Proc. 14th Int. Conf. Rewriting Techniques and Applications (RTA'2003), Valencia, Spain, June 2003, volume 2706 of Lecture Notes in Computer Science, pages 180-196. Springer, 2003.

• Kumar Neeraj Verma. On closure under complementation of equational tree automata for theories extending AC. In Proc. 10th Int. Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'2003), Almaty, Kazakhstan, Sep. 2003, volume 2850 of Lecture Notes in Artificial Intelligence, pages 183-197. Springer, 2003.

• H. Comon-Lundh and V. Cortier. New decidability results for fragments of first-order logic and application to cryptographic protocols. In Proc. 14th Int. Conf. Rewriting Techniques and Applications (RTA'2003), Valencia, Spain, June 2003, volume 2706 of Lecture Notes in Computer Science, pages 148-164. Springer, 2003.