This repository contains the EasyCrypt code associated with the paper "A. Buldas, D. Firsov, R. Laanoja, A. Truu. Verified Security of BLT Signature Scheme ".
- BLT_ReadOnly_Hashed/ - adversary has read-only access to hashed repository.
- BLT_ReadWrite_Hashed/ - adversary has read/write access to hashed repository.
- BLT_ReadWrite_Hashed_Set/ - adversary has read/write access to repository containing sets of hashed entries.
- BLT_ReadWrite_Plain/ - adversary has read/write access to the plain repository.
- BLT_ReadWrite_Hashed_MT/ - adversary has read/write access to the repository containing roots of Merkle Trees.
-
For this project we used the version of EasyCrypt (1.0) theorem prover with GIT hash: r2022.04-48-gc8d3d6c1.
-
EasyCrypt was configured with support from the following SMT solvers: [email protected], [email protected], [email protected], [email protected].
-
To check the development run:
$> cd DEVELOPMENT_FOLDER $> bash checkall
-
If you want to typecheck this code in Emacs then you must update your load path. Make sure your
~/.emacs
file contains the following load paths:'(easycrypt-load-path (quote ( "DEVELOPMENT_PATH/BLT_ReadOnly_Hashed" "DEVELOPMENT_PATH/BLT_ReadWrite_Hashed" "DEVELOPMENT_PATH/BLT_ReadWrite_Hashed_MT" "DEVELOPMENT_PATH/BLT_ReadWrite_Hashed_Set" "DEVELOPMENT_PATH/BLT_ReadWrite_Plain")))