Formal Techniques for Cryptographic Protocol Analysis (Laurea Magistrale in Matematica)

Informations

This page contains information about the course. It will be updated during the course, providing material and references.

In order to read the presentations, you will need LibreOffice or any other OpenDocument format reader.

Teaching material:

• Domain theory introduction
• On inference rules - short introduction
• Semantics of the lambda calculus - (Most of this is not required for the exam: see the slides)
• A very short introduction to the Curry-Howard isomorphism
• Adversary models: computational vs formal
• Brief introduction to the pi calculus and related formalisms to model crypto protocols
• Short notes on temporal logic and model checking
• Some negative results on automatic protocol verification
• Some very brief notions of abstract interpretation
• The Rewrite tool and related papers
• Rough sketch of some exercises on the second part

Please note that the presentations above can be updated without notice.

Some references and links:

• Some domain theory can be found in: The Formal Semantics of Programming Languages - G. Winskel
• The Coq Proof Assistant
  • Coq in a Hurry - quick introduction to Coq
  • If you wish to do practice with Coq, I recommend using the coqide environment.
  • Coq examples
  • The typing rule for dependent match (Coq source)
• A few references on the pi-calculus (optional material):
  • A Calculus of Mobile Processes, R. Milner - Part 1 Part 2
  • The Polyadic pi-Calculus: A Tutorial, R. Milner (the first part)
  • An Introduction to the pi-Calculus, J. Parrow (page 27 and discussion)
  • Pi-calculus: syntax and reduction semantics, F. Zappa Nardelli (slides)
  • On the pi-calculus, N. Yoshida (slides - in our course we did not cover the CCS part)

Assignments (optional)

Reminder: these are individual assignments, so working in groups is not allowed.

• To be announced on Moodle.

Exams

• Session 1: 2014-06-23 at 14:30 in room A213 - questions
• Session 2: 2014-07-24 at 14:30 in room A213 - questions
• Session 3: 2014-09-08 at 14:30 in room A213 - questions
• Session 4: 2015-01-12 at 14:30 in room A215 - questions
• Session 1: 2015-06-15 at 14:30 in room A215 - questions
• Session 2: 2015-07-07 at 14:30 in room A214 - questions
• Session 3: 2015-09-03 at 14:30 in room A215 - questions
• Session 1: 2016-06-13 at 14:30 in room B104 - questions
• Session 2: 2016-07-07 at 14:30 in room B104 - questions
• Session 3: 2016-09-05 at 14:30 in room B104 - questions
• Session 1: 2017-06-06 at 14:30 in room A107 - questions
• Session 2: 2017-07-07 at 14:30 in room A209 - questions
• Session 1: 2018-06-28 at 14:30 in room A213 - questions
• Session 2: 2018-07-06 at 14:30 in room A211 - questions
• Session 1: 2019-06-17 at 14:30 in room A224 - questions
• Session 2: 2019-07-11 at 14:30 in room A209 - questions
• Session 1: 2020-06-11 at 14:30 (Zoom) - questions
• Session 2: 2020-07-08 at 14:30 (Zoom) - questions
• Session 1: 2021-06-15 at 14:30 (Zoom) - questions
• Session 1: 2022-06-21 at 14:30 in room A223 - questions
• Session 2: 2022-07-14 at 14:30 in room A223 - questions
• Session 1: 2022-06-23 at 14:30 in room A209 - questions
• Session 2: 2022-07-19 at 14:30 in room A212 - questions

Home - Teaching

Roberto Zunino, 2014