Computationally soundformal blind signature
Hideki Sakurada
NTT Communication Science Laboratories
Nippon Telephone and Telegraph Corporation

Joint work with Masami Hagiya

Motivation• Bridging the gap between– Computational, probabilistic model– Symbolic, non-deterministic modelof protocol security [Micciancio-Warinschi][Cortier-Warinschi]• Symbolic model with blind signature [Kremer-Ryan]– Voting protocols and digital cash protocols

Contributions
1. Construct symbolic modelwith blind signature
Computational model

Symbolic model

Assumptions onblind signature

Adversary’s ability
2. Provesoundness

Blind Signature Scheme• Enables user to obtain signature σ to message mkeeping m secret to signer (blindness)• In voting scheme, voter is enabled to obtain ballot
σ keeping his vote m secret to administrator
Userm, vk

Signersksk

β ←Blind(vk, r, m) βγγ←Bsign(sk, β)σ←Unblind(r, γ)(m, σ) s.t. Verify(vk, m, σ)=1

Symbolic Blind Signature
Userm, vk
β ←Blind(vk, r, m)σ←Unblind(r, γ)

Blind(r, M)
Bsign(Blind(r, M))

Signerskskγ←Bsign(sk, β)Sign(M)• How can we define symbolic adversary’s ability
reflecting assumptions in computational model?

Computational Assumptions
1. Blindness： Information on message m is notrevealed from blinded message β←Blind(vk, r, m)
2. Unforgeability： Number of sigs. obtained by adv≤ Number of times signer signs
Adversary(User)

Challenger(Signer)sk…

(m1, σ1),…,(mn, σn)s.t. mi≠ mj, V(vk, mi, σi)=1

E.g. FDH-RSA blind signature• Adversary may not follow the scheme toobtain valid signature
SignerAdversaryr ←Zn*β ←re·H(m)β (・)1/2σ ←r-1 · γ

γ (・)2(m, σ)γ ←β dAdversary’s blinded message• Introduce adversary’s blinded message Blindadv
to the symbolic model• Also represents “irregular” blinded message
AdversaryBlindadvr ←Zn*β ←re·H(m)Signerβ (・)1/2
Bsign(Blindadv)

σ ←r-1 · γ(m, σ)γ (・)2γ ←β dSymbolic Adversary’s Ability• From a set Γ, adv. can obtain message m
1. Deducible by the rules below, where
2. Num. of times he uses the unblind rules≤ Num. of Bsign(Blindadv) received• No rule for Blind(r, M) because we assume
honest party never disclose random r
unblindExamples• Symbolic adversary can not deduce
Blindness

Unforgeability

computational
protocol runs

Soundnesssecure runs⊆⊆

(except withnegligible prob.)

symbolic
protocol runs

imply

∼

secure runs

Mapping Lemmacomputational
protocol runs

symbolic
protocol runs

∃f→ ⊆(except withnegligible prob.)⊆⊆secure runs

f-1

⊇ ←∼

secure runs

Outline of Proof
Similar to [Cortier-Warinschi]

I.

Construct mapping from computational runs into
symbolic runs:<“blind”, m> a Blind(r, M), if generated by honest partya Blindadv,
otherwise<“bsign”, m>a Bsign(Blind(r, M)),
if successfully unblinded and verified

II. Show the symbolic runs satisfy the conditions
1. Message sent by adv. can be deduced by the rules
2. Num. of signadv(-) ≤ Num. of bsign(blindadv)

If the cond.1 is not satisfied

Honest parties
Blind(r, n)
…n …

Adv.

If the cond.1 is not satisfied
Adversary of blindness game
Choose n0, n1

Challenger
Choose b←{0,1}n0 , n1Play
User0(vk, nb)

Blind(r, nb)

User1(vk, n1-b)

Simulate honest parties
by using challenger

Adv.
of Protocol

Blind(r, mb)

Blind(r, n1-b)…nb …
Output b’ = 1 if nb=n1b’

If the cond.2 is not satisfied
Adversary

Honest parties
Bsign(Blind(M0))
Bsign(Blind(M1))
Bsign(Blindadv)

Signadv(M’1)
Signadv(M’2)

If the cond.2 is not satisfied
Adv. of unforgeability gameAdv. prot.

Challenger(Signer)

Bsign(Blind(M0))
Bsign(Blind(M1))
Bsign(x)Sign. to M0

Sign. to M’1

Sign. to M1

Sign. to M’2Wins the unforgeability game.

Case 2Adversary

Honest parties
Bsign(Blind(M0))
Bsign(Blind(M1))
Bsign(Blindadv)

Signadv(M1)Signadv(M3)Adv. obtains information on M1 .
Similar to Case 1.

Conclusion• We have constructed a symbolic protocol
model with blind signature• Shown the soundness of the model withrespect to the computational model where– Blindness– Unforgeabilityof blind signature are assumed.