Verifying security protocols (Rust)
Supervisor
Suitable for
Abstract
Sigma protocols are a particularly simple and efficient kind of zero-knowledge proof and have seen wide deployment; they remain a leading kind of proof both in terms of simplicity and deployment but recent advances in succinct zero-knowledge proofs offer greater efficiency. The first efficient sigma protocol was introduced by Schnorr [2], several years before the class was defined. You can read more about sigma protocols in chapter 5 of this book [1].
To give you some insight into sigma protocols, we briefly discuss the most famous sigma protocol, the Schnorr protocol [2]. Given some public input (G, g, q, h) where G is a cyclic group of prime order q, and g and h are two generators of the group G, the prover claims that she knows a witness w for the statement h = g^w; the existence of such a w is immediate because g generates the group. However, does the prover know the witness w? In order to convince the verifier, the prover and the verifier do the following:
- the prover picks a random number u, computes c = g^u, and sends c to the verifier
- the verifier picks a random challenge e and sends it to the prover
- the prover computes t = u + e ∗ w and sends t to the verifier
The verifier accepts if g^t = c ∗ h^e, otherwise rejects.
In this project, the goal is to use session types to capture the communication between the Prove and the Verifier. It is a very simple binary session type with three messages. Our first step will be to encode the Schnorr protocol, described above, in NuScribble, generate Rust API fron NuScribble encoding, and fill the rest of the cryptographic code. Later, we will develop the Parallel composition, AND composition, OR composition, and NEQ composition of sigma protocols (see the chapter 5 of [1])
[1] https://www.win.tue.nl/~berry/2WC13/LectureNotes.pdf
[2] https://link.springer.com/article/10.1007/BF00196725