As of SSProve v0.3.0, the features of Nominal-SSProve have been completely integrated into SSProve. Therefore, this repository has a new purpose: To showcase developments that use Nominal-SSProve.
Nominal-SSProve v1.1.7 is the last version of this repository with an independent development of nominal properties. The properties as integrated into SSProve are found here.
Install dependencies by entering the nix development environment with command nix-shell or using the docker environment as described below.
It is recommended to use the coq, coq-community and math-comp nix caches to significantly reduce initial build time.
Check all project files using make and inspect files using vim (with Coqtail) or CoqIDE.
Build image with Coq dependencies and enter shell with commands:
docker build -t nominal-ssprove .
docker run --rm -it nominal-ssprove
The project files are copied into the image, so changes made will not propagate to the host filesystem.
The final image is around 4GB in size and can be deleted with the command docker rmi nominal-ssprove.
- Sigma-protocols in Nominal-SSProve: MarkusKL/ssprove-sigma
- PKE-example in SSProve: SSProve/ssprove
Student projects using Nominal-SSProve:
- Development of DDH and KEM based CKA: hrallil/nominal-ssprove
- Cryptobox in SSProve based on Bringing SSPs to EC: Myssenberg/nominal-ssprove
- Building Commitment Schemes from Sigma-protocols: petersabroe/thesis