- Notifications
You must be signed in to change notification settings - Fork0
dfirsov/comparison-based-non-malleabiltiy-unsat
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
This repository contains the EasyCrypt code associated with the paper "D. Firsov, S. Laur, E. Zhuchko.Unsatisfiability of Comparison-Based Non-Malleability for Commitments" published at ICTAC 2022.
- checkall - script for running the EasyCrypt proof-checker on the entire development.
- CNM_unsat.ec - definition of comparison-based non-malleability and the proof of its unsatisfiability:
lemma cnm_unsatformalizes Thm. 1 from Sec. 2.1.
- D1D2.ec,WholeMsg.ec - auxiliary games
- For this project we used the developement version of EasyCrypt (1.0) theorem prover with GIT hash: r2022.04-23-gb44893a5
- EasyCrypt was configured with support from the following SMT solvers: Why3@1.5.0, Z3@4.8.7, CVC4@1.6, Alt-Ergo@2.4.1
- to check the development run:
$> cd DEVELOPMENT_FOLDER && bash checkall
About
EasyCrypt proof of unsatisfiability of comparison-based definition of non-malleability for commitments
Topics
Resources
Uh oh!
There was an error while loading.Please reload this page.
Stars
Watchers
Forks
Releases
No releases published
Packages0
No packages published
Contributors2
Uh oh!
There was an error while loading.Please reload this page.