Summer school: Models and Tools for Cryptographic Proofs
The slides of the course are available here.
The goal of the exercise session is to model and analyse protocols using ProVerif. Please first install ProVerif.
- First model the Needham-Schroeder protocol.
- You may start from this truncated file.
- Model secrecy of the nonce Nb sent by B.
- Retrieve the attack.
- Modify your ProVerif file in order to model Needham-Schroeder-Low protocol.
- Prove secrecy of the nonce Nb and authentication between A and B.
- Model more protocols. At least 3 of these 5 protocols are flawed. Which ones? (You don’t need to read French)
