Equality of Discrete Logarithms

The voter’s computerP uses the encryption algorithmE. We want to make sure thatP computes correctly during the encryption. For this, we will use a proof that two elements have the same discrete logarithm relative to two distinct generators of the groupG. The proof isπ_E, and is between a proverP_eqdl^I and a verifierV_eqdl^I .

The ballot boxBuses the transformation algorithmT. We also want to make sure that Bcomputes correctly. For this, we will need two equality of discrete logarithms proofs.

6

One that proves that several group elements are raised to the same power as a certain element, and one that proves that several elements has been correctly raised to distinct powers. The proofs areπ_TIandπ_TII, respectively, and are between a proverP_eqdl^II and a verifierV_eqdl^II , and a proverP_eqdl^III and a verifierV_eqdl^III , respectively.

The three proofs above, must all satisfy the three propertiesCompleteness, SHVZK,and Soundnesswith definitions given below.

Completeness Any proof generated by an honestPmust be accepted byV.

Special Honest Verifier Zero Knowledge That the proof is SHVZK means that on a given challenge e, a simulator should be able to choose a random ν which produces transcripts indistinguishable from the real ones. The simulator will not get the private input w.

Soundness LetRel(s, w)be the relation between the statementsand the witnessw. It must be hard to generate valid proofs when the relation does not hold.

Proof of correct computation I

We want to prove that two element have the same discrete logarithm relative to distinct generators of the groupG. Both the prover and the verifier are given as public input some auxiliary informationaux, two generatorsgand¯gofG, and the commitmentsx,x. The¯ prover is in addition given the private input integert. The relation isRel(x, t) = (log_gx=^? log_¯gx¯=^? t).

For this equality of discrete logarithms problem, the prover and the verifier algorithms are:

π_E ← P_eqdl^I (aux, t;g,g;¯ x,x)¯ 1/0← V_eqdl^I (aux;g,g;¯ x,x;¯ π_E).

Instantiation A Σ3-protocol for the Equality of Discrete Logarithms with proverP, verifierV, statements= (aux, g,g, x,¯ x)¯ and witnesstsuch thatx=g^tandx¯= ¯g^tis:

The completeness condition requires that any proof generated by an honestP must be accepted byV.

Applying the Fiat-Shamir transformation we get the following.

LetH1:{0,1}^∗×G⁶→ {1,2, ...,2^τ}be a hash function in the random oracle model.

Then the prover will compute

e←H1(aux, g,¯g, x,x, α¯ 1, α2), and the verifier will compute

e⁰←H1(aux, g,g, x,¯ x, g¯ ^νx^e,g¯^νx¯^e).

The proof isπ_E = (e, ν), and the verifier will accept iffe⁰ =e.

Security analysis Two properties for the proofs are required: they most be zero knowl-edge and satisfy a soundness condition. For the zero knowlknowl-edge it suffices for the protocol to be Special Honest Verifier Zero Knowledge (SHVZK), the non-interactive proof will then be Non-interactive Zero Knowledge, with the hash oracle acting as an honest verifier.

For the Soundness property, there need to exist a simulator that on a given input produces a conversation with the same probability as in the real proof.

Completeness An honest P will on statement (aux, g,g, x,¯ x)¯ generate a proof (e, ν) = (H1(aux, g,g, x,¯ x, g¯ ^u,g¯^u), u−etmodq). The verifierV will then compute e⁰ =H1(aux, g,g, x,¯ x, g¯ ^νx^e,¯g^νx¯^e). It is easy to see thate⁰=eif the relation holds, and hence the proof will be accepted byV.

Special Honest Verifier Zero Knowledge Given any challengee, we can choose a randomνand computeα1=g^νx^eandα2= ¯g^νx¯^e, withx=g^tandx¯= ¯g^t. It is easy to see thatα1andα2has the same distribution as in the real proof.

Non-interactive Zero Knowledge An interactive proof that is SHVZK becomes Non-interactive Zero Knowledge (NIZK) when the Fiat-Shamir Transformation is applied to make the proof non-interactive.

ProverP^H1

Let a left game LHS be as above. An adversary A have access to a random oracle H₁and outputs a statementsand a witnesst. The proverP (with access to the same random oracle) follows the protocol as before, and then sends the proof(e, ν)toA. The adversary then tries to distinguish between the real proof and the simulation.

SimulatorSIM^S An adversaryAhave access to the simulatorSand outputs a statementsand a witnesst.

The simulatorSIM(with access toS) usesSto gete,Sim^I_eqdl(aux;g,¯g;x,x, e)¯ to get νand then sends the proof(e, ν)toA. The adversary then tries to distinguish between the real proof and the simulation.

LHSZK_L

The advantage of the adversary is

Pr[A^H1(e, ν) = 1|(e, ν)← P^{$ H1}]−Pr[A^S(e, ν) = 1|(e, ν)← SIM^{$ S}] . Soundness Probability bounds for the adversary being able to forge proofs when the relation does not hold are given in the following propositions.

Lemma 2.10.1. LetGbe a group of prime orderq, and letgand¯gbe generators ofG.

Supposetand∆,∆6= 0are integers, andg,g, x,¯ x, α¯ 1, α2are group elements such that x=g^tandx¯= ¯g^u+∆. Letebe an integer choosen uniformly at random from{1, ...,2^tau}.

Then the probability that there exists an integerνsuch that α1x^−e=g^νandα2x¯^−e= ¯g^ν is at most1/2^τ.

Proof. Letα₁=g^uandα₂= ¯g^u+δforδan integer. Then the relations will be u−et≡νmodqandu+δ−et−e∆≡ν modq.

For this to be satisfied, we must have that

δ−e∆≡ν modq.

Bothδand∆are fixed beforeeis sampled, so the probability of this event is at most

1/2^τ.

Theorem 2.10.2. For any algorithmAthat makes at mostηqueries to the random oracle H₁and outputs a proofπ_E and statements, where the relationlog_gx= log_¯gx¯does not hold, then

V_eqdl^I (s, π_E) = 1 with probability at most2η/2^τ.

Proof. If the algorithm has not already queriedH₁at the relevant point, the proof verifies with probability1/2^τ.

By Lemma 2.10.1, the adversary has a probability of at most1/2^τof forging a proof every time she queriesH₁.

We now have at mostη+1event, each with probability at most1/2^τ, and the probability that at least one of them happen can be bounded as

1−

Proof of correct computation II

We need to prove that we have raised a number of group elements to the same power. The proof isπ_TIwith the prover’s and the verifier’s algorithms as follows:

πTI ← P_eqdl^II (aux, g, γ, s;w1, ..., wk,wˇ1, ...,wˇk) 1/0← V_eqdl^II (aux, g, γ;w₁, ..., w_k,wˇ₁, ...,wˇ_k;π_TI).

10

The public input which both the prover and the verifier gets, is some auxillary information aux, a generatorg, a commitmentγ, and the group elementsw₁, ..., w_k,wˇ₁, ...,wˇ_k.The prover’s private input is the integerssuch thatγ=g^sandw^s_i = ˇw_i, i= 1, ..., k.

Completeness is also required here.

Instantiation The verifier chooses random e1, ..., ek from{1, ...,2^τ} and sends~e = (e1, ..., ek)to the prover.

The prover computesx= Π^k_i=1w_i^ei, choosesuat random fromZ^q, computesα1= g^u, α2=x^uand send(α1, α2)to the verifier.

The verifier chooses randomefromZ^q and send it to the prover.

The prover computesν←u−semodq, and sendsνto the verifier.

The verifier computesx= Π^k_i=1w^e_iⁱandxˇ= Π^k_i=1wˇ^e_iⁱand accepts iff α₁=g^νγ^eandα₂=x^νxˇ^e.

Now, apply the Fiat-Shamir transformation to get the proof non-interactive. Let a hash functionsH₁:{0,1}^∗×G^2k+2→ {1, ...,2^τ}^kandH₂:{0,1}^∗×G^2k+2→ {1, ...,2^τ}

Security analysis As before, zero knowledge and soundness is required.

The protocol is SHVZK because there exists a simulator that for a givene, samplesνat random and outputs it,ν←Sim^II_eqdl(aux, g, γ, ~w, ~w, ~ˇ e, e). Then it is clear thatα1=g^νγ^e andα2=x^νxˇ^ewithxandxˇas above have the same distribution as in the real protocol.

Applying the Fiat-Shamir transformation then yields a non-interactive zero knowledge proof. Generate this proof by first sampling aneat random, queryH1to get~e, useSim^II_eqdl to getν, and then reprogram theH2oracle appropriately.

This proof is sound in the Random Oracle Model and a soundness bound is given below.

Lemma 2.10.3. LetV be any proper subspace ofF^kq, and letSbe a subset ofFq with 2^τ elements. Samplee₁, ..., e_kindependently and uniformly at random fromS. Then the probability that~elies insideV is at most1/2^τ.

Proof. The proof is given in [ste13].

Lemma 2.10.4. LetGbe a group of prime orderqandga generator of it. LetS be a subset ofZ^q with2^τelements. Supposes,∆1, ...,∆kare integers such thats6≡0 modq and∆j = 0 for at least onej. Letw1, ..., wk,wˇ1, ...,wˇk be group elements such that

ˇ

wi=w^s_ig^∆i,i= 1, ..., k.

If∆_i6≡0 modqfor anyi, ande₁, ..., e_kare integers chosen uniformly at random from a set with2^τelements, then

Π^k_i=1wˇ^e_iⁱ= (Π^k_i=1w^e_iⁱ)^s (2.2) holds with probability at most1/2^τ.

Proof. The equationΣ^k_i=1∆iei ≡0 modqdefines a proper subspace ofF^kq. If equation (2.2) holds, then Π^k_i=1g^∆iei = 1, or Σ^k_i

1 ≡ 0 modq. That is, (2.2) holds only if ~e considered as anF^q-vector falls inside a proper subspace ofF^kq. The claim then follows by

Lemma 2.10.3.

The last lemma needed for soundness is similar to the one above, 2.10.1, with the proof being similar as well.

Theorem 2.10.5. For any algorithm that makes at mostηqueries overall to the random oraclesH1andH2, outputs a proofπ_TI= (e, ν), a bit stringaux, an integers, and group elementsg, γ, w1, ..., wk,wˇ1, ...,wˇksuch thatw_i^s6= ˇwifor some i, then

V_eqdl^II (aux, g, γ, ~w, ~w;ˇ π_TI) = 1 holds with probability at most2η/2^τ.

Proof. If the algorithm has not already queried bothH1andH2at the relevant points, the proof verifies with probability1/2^τ.

By Lemma 2.10.4, the adversary has a probability of at most1/2^τof forging a proof every time she queriesH₁.

By Lemma 2.10.1, the adversary has a probability of at most1/2^τof forging a proof for some input by which she cannot already create a forged proof for, every time she queries H₂.

We now have at mostη+1event, each with probability at most1/2^τ, and the probability that at least one of them happen can be bounded similar as in equation (2.1).

Proof of correct computation III

We need to prove that a single group element has been raised to correct, distinct powers.

The proof isπ_TIIwith the prover’s and the verifier’s algorithms as follows:

πTII← P_eqdl^III (aux, g,x, yˇ 21, ..., y2k, a21, ..., a2k; ˆw1, ...,wˆk) 1/0← V_eqdl^III (aux, g,x;ˇ y₂₁, ..., y_2k,wˆ₁, ...,wˆ_k;π_TII).

Both the prover and the verifier receive the public input consisting of some auxilliary informationaux, a generatorg ofG, the commitmentsy2i, ..., y2k, the basexˇand the powerswˆ₁, ...,wˆ_k. The prover in addition gets the private input the integersa₂₁, ..., a_2k.

Completeness is also required here.

12

Instantiation The verifier chooses random e₁, ..., e_k from{1, ...,2^τ} and sends~e = (e₁, ..., e_k)to the prover.

The prover choosesuat random fromZq, computesα₁ = g^u, α₂ = ˇx^u and send (α₁, α₂)to the verifier.

The verifier chooses randomefromZ^q and send it to the prover.

The prover computesν←u−eΣ^k_i=1eia2imodq, and sendsνto the verifier.

The verifier computesy2= Π^k_i=1y_2i^eiandwˆ= Π^k_i=1wˆ^e_iⁱ, and accepts iff α1=g^νy^e₂andα2= ˇx^νwˆ^e.

Now, apply the Fiat-Shamir transformation to get the proof non-interactive. Let a hash functionsH1:{0,1}^∗×G^2k+2→ {1, ...,2^τ}^kandH2:{0,1}^∗×G^2k+2→ {1, ...,2^τ}

Security analysis As before, zero knowledge and soundness is required.

The protocol is SHVZK because there exists a simulator that for a givene, samplesνat random and outputs it,ν ←Sim^III_eqdl(aux, g,x, ~ˇ y₂, ~w, ~ˆ e, e). Then it is clear thatα₁=g^νy₂^e andα₂= ˇx^νwˆ^ewithy₂andwˆas above have the same distribution as in the real protocol.

Applying the Fiat-Shamir transformation then yields a non-interactive zero knowledge proof. Generate this proof by first sampling aneat random, queryH1to get~e, useSim^III_eqdl to getν, and then reprogram theH2oracle appropriately.

This proof is sound in the random oracle model and a soundness bound is given below.

Lemma 2.10.6. Let Gbe a group of prime orderqandg a generator of it. Suppose a21,...,a_2k,∆1, ...,∆kare integers andx, yˇ 21, ..., y2k,wˆ1, ...,wˆkgroup elements such that y2i=g^a2iandwˆi= ˇx^a2ig^∆i,i= 1, ..., k.

If∆i6≡0 modqfor anyi, ande1, ..., ekare integers chosen uniformly at random from a set with2^τelements, then the probability that there exists an integerasuch that

Π^k_i=1y^e_2iⁱ =g^aandΠ^k_i=1wˆ^e_iⁱ = ˇx^a (2.3) holds with probability at most1/2^τ.

Proof. If the left part of (2.3) holds, thenΠ^k_i=1g^∆iei = 1orΣ^k_i=1∆_ie_i ≡ 0 modq. So (2.3) only holds if~econsidered as anF^q-vector falls inside the previously defines proper subspace ofF^kq. The claim then follows by Lemma 2.10.3.

The last lemma needed for soundness is similar to the one above, Lemma 2.10.1, with the proof being similar as well.

Theorem 2.10.7. For any algorithm that makes at mostηqueries overall to the random oraclesH₁andH₂, outputs a proofπ_TII= (e, ν), a bit stringaux, integersa₂₁, ..., a_2k, and group elementsg,x, yˇ ₂₁, ..., y_2k,wˆ₁, ...,wˆ_ksuch thaty_2i=g^a2ifor alli, butˇx^a2i6=

ˆ

w_ifor some i, then

V_eqdl^III (aux, g,ˇx, ~y2, ~w;ˆ π_TII) = 1 holds with probability at most2η/2^τ.

Proof. If the algorithm has not already queried bothH1andH2at the relevant points, the proof verifies with probability1/2^τ.

By Lemma 2.10.6, the adversary has a probability of at most1/2^τof forging a proof every time she queriesH1.

By Lemma 2.10.1, the adversary has a probability of at most1/2^τof forging a proof for some input by which she cannot already create a forged proof for, every time she queries H₂.

We now have at mostη+1event, each with probability at most1/2^τ, and the probability that at least one of them happen can be bounded similar as in equation (2.1).

14

Chapter 3

Formal verification

Formal verification is proving the correctness of algorithms with respect to formal specifi-cations. Tools for formal verification may be used to prove (or disprove) the correctness of cryptographic protocols. The pen and paper proofs often uses the provable security approach, in which mathematical problems are tried reduced to attacks on the cryptographic construction. These proofs are often long and complicated. Tools where one may formalize systems and write proofs, and interactively verify steps on the way, may be used to increase confidence in such reductionist proofs.

3.1 EasyCrypt

EASYCRYPTis a tool for reasoning about probabilistic relational properties and the security of cryptographic constructions with adversial code. Is is used to construct and verify game-based cryptographic proofs. Four logics are used: Hoare logic, probabilistic Hoare logic, relational probabilistic Hoare logic, and ambient logic. SMT-solvers are able to automatically prove certain simple ambient logic goals.

EASYCRYPT has been used to provide machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model [War17] [cat17].

In document Formal verification of the Norwegian Internet Voting Protocol (sider 14-23)