I am currently working on designing a security protocol which involves usage of fuzzy commitment schemes, for. eg Reed-Solomon codes which allows us to tolerate a certain level of error.

I was wondering how one would go about formally verifying a security protocol which would use a scheme such as Reed-Solomon codes.

I searched online, and found out about tools out there such as AVISPA. ProVerify and even Casper/FDR which would help me test security protocols, however they do not seem to work with fuzzy commitment schemes.


This might not be the answer you are looking for, but as you are looking for a formal verification, I would advise you to take a look at Coq. Even though mainly used by Academics, it provides a logical framework and an interface to write formal and interactive proofs.

Based this language there exists some libraries dedicated to cryptographic proof :

Example of proof :

PHD : Formal certification of game-based cryptographic proofs

Other formal tools (interactive provers) can be used such as Isabelle, Agda, Fstar and HOL. And some more readings :

Disclaimer: I use Coq on daily basis...

  • $\begingroup$ Thank you @Biv. Coq seems interesting . Let me have look into it and get back to you. $\endgroup$ – FunnyPanda Mar 12 '16 at 0:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.