Handshake protocol verification in ProVerif
The protocol was updated so that the injective correspondence holds properly. Removing (hopefully) the possibility of a replay attack
- Generated a new nonce at the beginning of Alices process
- Alice sends nonce to Bob in public
- Bob receives nonce and adds it to his signature
- Alices confirms that the nonce in the signature is the same as she generated.