DY*, proof of concept with extrinsic proofs

What is in this repository

The "core" DY*

In the namespace DY.Core, we can find all functions and theorems needed to specify a cryptographic protocol and prove its security. To read and understand this module, you can start by reading the file DY.Core.fst.

The "lib" DY*

To improve the user experience of specifying cryptographic protocols and doing security proofs, we can find functions and theorems built on top of DY.Core in DY.Lib.

Examples

The NSL protocol has been proven secure in the namespace DY.Example.NSL, and the ISO-DH protocol has been proven secure in the namespace DY.Example.DH.

How to build

Dependencies

DY* depends on the F* proof-oriented programming language, and depend on Comparse, a library for message formats in F*.

Two choices are possible:

• either Comparse is cloned in ../comparse and fstar.exe is in the PATH
• or Comparse is cloned in COMPARSE_HOME and FSTAR_EXE is set to the location of fstar.exe, in that case using direnv is a advisable.

Compiling

Running make will compile and verify DY* and its examples.

How to contribute

Please read the CONTRIBUTING document.