Computational Soundness of (Interactive)
Zero-Knowledge Proof Systems
in the Presence of Active Adversaries
Yusuke Kawamoto1(Jointly with Gergei Bana2 and Hideki Sakurada3)
1 University of Tokyo

2 Technical University of Lisbon
3 NTT Communication Science Labs.

Computational Soundness
Computationalsoundness

Our Contributions• Applied pi-calculus for protocols using Interactive
Zero-Knowledge as sub-protocols• Soundness of the observational equivalence of theapplied pi-calculus (ongoing)– Active & adaptive adversary– Interpretation (i.e. the way of relating symbolic processwith computational process) differs from previous work.
– Mapping soundness + Tree soundness
The proof of soundness issimilar to [Comon & Cortier’08]
Similar results on mapping soundness for
Non-Interactive Zero-Knowledge [Backes & Unruh’08]

Overview• Zero-Knowledge Interactive Proof System• Symbolic model (applied pi-calculus)• Computational Soundness• Conclusion & Discussion

PoK (Proof of Knowledge) for R∀(x, s)2R

witness

NP-relation(x, s)
ProverP

rs is not given to V

Random input

interaction

xVerifierVP knows some ys.t. (x, y)2RokNon-triviality of PoK∀(x, s)2R∀r2 Random(x, s)

Prs is not given to Vrx

ProverVerifier

PV=1okValidity of PoK∀(x, s)2R∀

r2 Randoms is not given to Vx

IfPr

OracleVerifierP *x, s, rV: non-negligible

okthenPr

V can access to oracle many times
on the same random input r.

OracleP *x, s, r⋮xExtractor∃

K: non-negligibles

(Concurrent) Zero-Knowledge of PoK• Adversary cannot obtain any information of thewitness from provers running concurrently.
• Formally, for any PPT adversary V*, there is PPT SV* s.t.
V * ’s view and its simulation are indistinguishable.
∀x∈LR ∀y∈{0,1}*

V * interacts with honest Pon input x.

(x, s1)x, yx, yPV*(x)

V*!

P…

…

(x, sn)Adversary¼
indistinguishable

Simulator∃

SV*Our Computational Model• Zero-Knowledge PoK (Proof of Knowledge)– Assume Non-triviality, Validity & Concurrent Zero-Knowledge• One-way collision-free function f• Each agent transmits bit strings:– Messages in PoK are explicitly transmitted.

• Adversary is probabilistic polynomial-time.

Example: Group Identification Protocol
PoK for R={(x, s)| x∍f(s)}All encrypted passwords

One-way collision-free function
No one can derive x from f(x).

User Pi ’s password({f(si) | i∊G}, si){f(si) | i∊G}
si is not given to V

UserServerPiVExample: Group Identification Protocol
PoK for R={(x, s)| x∍f(s)}All encrypted passwords

One-way collision-free function
No one can derive x from f(x).

User Pi ’s password({f(si) | i∊G}, si){f(si) | i∊G}

UserServerPiVokV can learn no
information of si

Pi knows some ss.t. {f(si) | i∊G} ∍ f(s)V learns that the prover is in the group G

Example: Group Identification Protocol
PoK for R={(x, s)| x∍f(s)}All encrypted passwords

User Pi ’s password({f(si) | i∊G}, si)

One-way collision-free function
No one can derive x from f(x).
When a group is created, user’s
password is randomly generated.

{f(si) | i∊G}

UserServerPiVokV can learn no
information of si

Pi knows some ss.t. {f(si) | i∊G} ∍ f(s)V learns that the prover is in the group G

Example: Group Identification Protocol
PoK for R={(x, s)| x∍f(s)}All encrypted passwords

User P0 ’s password{f(si) | i∊G}({f(si) | i∊G}, s0)

Adversary

P0

V*(x)
V*

¼Simulator

by Concurrent zero-knowledge

SV*

Anonymity¼{f(si) | i∊G}({f(si) | i∊G}, s1)
User P1 ’s password

P1

Adversary

V*(x)
V*

Overview• Zero-Knowledge Interactive Proof System• Symbolic model (applied pi-calculus)• Computational Soundness• Conclusion & DiscussionTerms• Agents transmit symbolic messages (Dolev-Yao terms).
• We introduce terms that abstracts ZKIP.
Term ::= Name Password
One-way collision-free function
No one can derive x from f(x).
| f(Name)| { Term, Term } | π1(Term) | π2(Term)| ok | ⊥| v(Term) | πv1(Term)| w(Term , Term, Term) | πw1(Term) |πw3(Term)
These terms abstracting ZKIP correspond toa lot of messages in interactive proofs incomputational setting.

Conditions• Agents & adversary can use the condition tests:Well-formedness of terms
Φ ::= M(Term)
Equality as bit strings| EQ(Term, Term)| Verify(Term , Term, Term)| Φ∧Φ | Φ∨ ΦNo negation
Check whether the interactive proof is true or not.

Symbolic Process• General definition of Process (similar to [Comon &Coriter’08])

Process Running PoK
Computational PoK

User iAdversaryServerx(x, si)……

……

A lot of interaction

okokProcess Running PoK

Bad Definition

Symbolic PoKUser iAdversaryComputational PoK

ServerUser ix(x, si)(x, si)w(x, si)AdversaryServerxw(x, si)

A lot of interaction

okw(x, si)……

……

Adversary can reuse the proof
and pretends to be User i
without the password si(He cannot reuse it in comp.)

okokProcess Running PoK
Symbolic PoK

Computational PoK

User iServerUser i(x, si)x(x, si)AdversaryServer
xv(x)

n

……

……

w(x, si, n)A lot of interaction

okok
Messages during PoK processes isabstracted into 3 messages.

okProcess Running PoK
Symbolic PoKAdversaryUser i

Server(x, si)

xv(x)

nv(x)

n
Verification of ZKIP

w(x, si, n)okP(x, si)w(x, si, n)same n?

oksame x?
?
f(s)∈ xV(x)Process Running PoK
Symbolic PoKAdversaryUser iServer(x, si)

xv(x)

nv(x)

n
Verification of ZKIPAdversary can’t producew(x, si, n)okP(x, si)V(x)w(x, si, n)okw(x, si, n)

Another sessionn’Adversary cannot reuses
this proof in anothersession that uses
another nonce n’.

Overview• Zero-Knowledge Interactive Proof System• Symbolic model (applied pi-calculus)• Computational Soundness• Conclusion & Discussion

Computational Soundness
Computationalsoundness

Outline of Proof
The proof of soundness is similar to [Comon & Cortier’08]

Tree Soundness(Concurrent Zero-knowledge)«P¼ OTP ¼ OT1 ¼ OT2 … ¼ OTn ¼

OT Q¼ « «Q ¬Mapping Lemma(Validity, Concurrent Zero-knowledge, One-wayness, collision-freeness)

Conclusion• Applied pi-calculus for protocols using Interactive
Zero-Knowledge (of knowledge)• Soundness of the observational equivalence of theapplied pi-calculus (ongoing)– Active & adaptive adversary– Interpretation differs from previous work.
– Mapping soundness + Tree soundness

Related Work
• Soundness of symbolic Non-Interactive ZK [Backes andUnruh]– Our work deal with interactive ZK.
• In their symbolic model, a prover sends a proof term.
• In our model, Messages during PoK processes is abstracted into 3messages.

– Our work includes not only mapping but also tree soundness.
– Assumption on ZK• They assumed Non-malleability of ZK proofs.
• Our work does not assume it, and restricts the class of protocols.

• Universally composable ZK– Universally composable ZK requires CRS model.
– Our work deals with Concurrent ZK that is weaker than
Universal Composable ZK.
– Composition of soundness result is our future work.

Thank you for your attention.