Summer school: Models and Tools for Cryptographic Proofs
The slides of the course are available here.
- 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)