Simple way to do ZK using protocol analysis tools
Formal methods analysis can be limited in functionality and modelling ZK is hard...
Last week, I was using Verifpal to model a new password-authenticated key exchange (PAKE). In this PAKE protocol, several steps included the use of zero-knowledge proofs, which are traditionally very hard to model in these tools. This left me a bit frustrated as I couldn’t do the task I wanted to do…
After thinking about this for a bit, I believe I have found a very simple solution (many will say it’s trivial) to emulate this primitive using only hashes.
(Note: In this post, I’m *not* going to cover zero-knowledge, PAKE, etc… I’ll leave that as an exercise for the readers who may not already be familiar with these topics.)
Back to Verifpal and modelling ZK proofs!
Verifpal is a software that allows practitioners to quickly run a software check on the design of cryptographic protocols. Traditionally, tools like Tamarin Prover, ProVerif, CryptoVerif, or CPSA are more respected in the cryptography community. I prefer to use Verifpal (as it allows me to iterate far more quicker than using other tools).
A big limitation of many of these tools, however, is the lack of support for ZK proofs. I came up with the simple design to model such primitive.
Here’s my suggestion:
Prover generates a public value “x” (the statement)
Prover generates a secret value “w” (the witness)
Prover obtains proof = Hash(x, w)
[the actual variable result = Hash(proof)]
Prover → Verifier : Hash(x, w)
[Verifier should know a variable called expected_value (which is equal to result)]
Verifier hashes the received value
Verifier compares the obtained hash digest with expected_value
That’s it!
We preserve “soundness” because no adversary is able to produce a preimage that matches the result.
We preserve “completeness” because only the prover that knows the secret witness can produce the proof.
We (kind of) preserve “zero-knowledge” because there is no leak of information to any adversary regarding the actual secret value. (The code does not represent complete zero-knowledge, but it’s just an approximation”