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
.
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
.
The NSL protocol is proved secure in the namespace DY.Example.NSL
.
DY* depends on the F* proof-oriented programming language, and depend on Comparse, a library for message formats in F*.
Two choices are possible:
../comparse
and fstar.exe
is in the PATH
COMPARSE_HOME
and F* in FSTAR_HOME
,
in that case using direnv is a advisable.Running make
will compile and verify DY* and its examples.
Please read the CONTRIBUTING document.