Tamarin proof scripts
This folder contains formal models of some cryptographic protocols used in picoTalk. The models are written for the Tamarin Prover. The idea is to automatically proove the relevant security properties of the non-standard protocols used in picoTalk.
Non-standard protocols include:
- The password authenticated key-exchange.
- The secure channel built on top of NaCl
- Triple-Diffie-Hellman (3DH) authenticated key-exchange (this is part of the Signal/Axolotl protocol though)