Schnorr Identification Protocol

Stream: new members

[minapw]

Hi. I’m new to lean and am having some trouble with my code. I want to write proofs of completeness and soundness for the Schnorr identification protocol. But first I obviously need to implement the protocol, which is where I’m struggling. The Schnorr protocol is a sigma protocol, wherein a prover wants to prove to a verifier that they have knowledge of a witness w, without revealing the witness. g is the generator of a group G, h = g ^ w.   The protocol goes like this:

Prover: picks a random number r. Sends a = g ^ r to verifier.  (r is not to be revealed to verifier)

Verifier:  picks a random number e. Sends e to prover.

Prover: Computes z = e * w + r. Sends z to verifier.

Verifier: Checks if g ^ z = h ^ e * a. If true, prover has successfully proven that they know a witness.

(g, e, a, z,h) are publicly available, but not r and w. r and e has to be chosen randomly each time the protocol is run.

I have two questions. Firstly, I am wondering about which type the different variables should be. And secondly why  I get this error message “failed to synthesize HPow G (ℕ → ℕ → ℕ → ℕ) ?m.8259  Additional diagnostic information may be available using the set_option diagnostics true command.” in the line def generator_z := x where z := response; x := g ^ z.

I’m taking inspiration from this implementation of elgamal  (https://github.com/JoeyLupo/cryptolib/blob/main/README.md  ).

I have written this code:

import Mathlib

/- Creating global variables.
-- G is the group that the generator g generates over.
-/

variable (G : Type)[inst_1 : Fintype G] [inst_2 : CommGroup G] [inst_3 : DecidableEq G]

          (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)

          (q : ℕ) [inst_4 : Fact (0 < q)] [inst_5 : NeZero q](G_card_q : Fintype.card G = q)

          (e : ℕ)

/-

Creating a namespace prover.

The variables are unavailable outside the namespace, but the functions are accessable.
-- w is the witness,
-- r is  a random number
-- h is g ^ w
-/

namespace prover

variable (w r : ℕ)

def commitment := g ^ r

def response := z where z := e * w + r

def response_gen := g ^ z where z := e * w + r -- this works, but generator_z does not

def return_h := g ^ w

end prover

open prover in

def generator_z := x where z := response; x := g ^ z -- this is where I get an error! Specifically the error is under g ^ z

/-

failed to synthesize

  HPow G (ℕ → ℕ → ℕ → ℕ) ?m.8259

Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/

´´´

[Johannes Tantow]

response is a function that takes three arguments e, w, r. Hence z is also a function with three arguments. There is no instance defined that has a function in the exponent. You need to pass values for e, w and r to the definition of generator_z and into z.

[minapw]

@Johannes Tantow that makes sense, thanks. I originally wanted w and r to be unobtainable outside of the namespace prover, is it possible to do this and also get the code to parse?

[(deleted)]

Why do you want them to be unobtainable in the first place

[(deleted)]

I feel this could indicate a misunderstanding of how proof assistants can be used to validate security properties

[Johannes Tantow]

Its not really obvious to me what you are trying to do. For now r and w are just arbitrary numbers. You can add functions that calculate r and w from some values and hide this via private.

[minapw]

r is a random number, and is supposed to be secret. Which is why I wanted verifier to only have access to g ^ r and not r itself. w is also secret, which is why I wanted r and w to only be available to the prover. That is what I try to achieve with the namespace prover. I wanted to make the response function so that the z is calculated using the w and r variables that I have defined in the namespace. But I'm not sure if that's what I'm actually doing ..

[Kenny Lau]

but you aren't inputting the real values of r and w into lean right? you're just verifying the algorithm works, so there's no need to hide r and w

[Johannes Tantow]

But then the function of the verifier could in principle only get a natural number and work with it. Then you could later prove that if this natural number has the form g^(z w r), then the algorithm/protocol is correct.

[Quang Dao]

You may be interested in ArkLib, a library for representing cryptographic proof systems & proving their security properties

As of right now, it is possible to use ArkLib for implementing Schnorr as a 3-message interactive argument, and prove completeness. Soundness is more tricky and we haven't defined rewinding extraction yet