Skip to content

Jasmin implementation of the eXtended Merkle Signature Scheme (XMSS) & proof of correctness in EasyCrypt

Notifications You must be signed in to change notification settings

ruipedro16/xmss-jasmin

Repository files navigation

xmss-jasmin

Proofs (for XMSSMT-SHA2_20/2_256)

Run

make -C proof/ check_spec
make -C proof/ check_xmss_xmssmt_proof
make -j$(nproc) -C proof/ check_correctness_proof
make -j$(nproc) -C proof/ check_correctness_proof ECADDFLAGS="-pragmas Proofs:weak"

Or, using docker

docker build -t jasmin-xmss .
docker run --rm -it jasmin-xmss

and then

make -C proof/ check_spec
make -C proof/ check_xmss_xmssmt_proof
make -j$(nproc) -C proof/ check_correctness_proof
make -j$(nproc) -C proof/ check_correctness_proof ECADDFLAGS="-pragmas Proofs:weak"

About

Jasmin implementation of the eXtended Merkle Signature Scheme (XMSS) & proof of correctness in EasyCrypt

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published