Simple end-to-end encrypted voice calls.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

574 B

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 secretbox.
  • Triple-Diffie-Hellman (3DH) authenticated key-exchange (this is part of the Signal/Axolotl protocol though)