Provable Anonymity
Epistemic Logic for Anonymizing Protocols
Ichiro Hasuo
Radboud University Nijmegen
The Netherlands

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 1/23

Introduction
Concern about on-line privacy is growing...
ISPs in EU might soon start logging all the URLs you
browseIntroduction● Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples

A number of anonymizing protocols have been introduced

Conclusion

Internatinal Summer School Marktoberdorf

Chaum Mix, Onion Routing, Crowds,...

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 2/23

Introduction
A lot of work in formal verification of authentication
protocols (e.g. Needham-Schroeder, Otway-Rees, ...) but
Introduction● Introduction

Formulation and verification of anonymity
is still quite immature

Example: onion routing
Semantics of epistemic
operators
Verification examples
Conclusion

Our work is first to
n comprehensively formulate competing notions for“anonymity”, andn actually verify real protocols,
using crypto-conscious epistemic logic

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 3/23

Coauthors

Introduction● Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples
Conclusion

Peter va? Rossum

Internatinal Summer School Marktoberdorf

Wolt?r Pieters?lavio D. Garcia

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 4/23

Coauthors

Introduction● Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples
Conclusion

Peter va? Rossum

Wolt?r Pieters?lavio D. Garcia

Full paper available:
Provable Anonymity.
F. Garcia, I. Hasuo, W. Pieters, and P. van Rossum.
To appear in FMSE 2005.
Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 4/23

Motivating example: onion routing
Introduced by [Chaum, ’81] and[Goldschlag, Reed, Syverson, ’96]
Introduction
Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic
Semantics of epistemic
operators
Verification examples

Practical implementation available asTOR (The Onion Router), http://tor.eff.org

Conclusion

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 5/23

Motivating example: onion routing
A tries to send a message m to B anonymously
Introduction
Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic{|−|}X : public-key encryption

ni : nonce

Semantics of epistemic
operators
Verification examples

A(((m)))

R1

((m))

R2

(m)

B

Conclusion(m) = {|m|}B((m)) = {|n1 , B, (m)|}R2(((m))) = {|n0 , R2 , ((m))|}R1

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 6/23

Onion routing
actual run
Introduction

A

B
((◦))

Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic

R
((•))

Semantics of epistemic
operators
Verification examples

(◦)

C

(•)
D

Conclusion

where

Internatinal Summer School Marktoberdorf((◦)) = {|n, X, (◦)|}R

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 7/23

Onion routing
actual run“counter” run
BA

Introduction((◦))

Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic

A

(◦)

B
((◦))

R
((•))

Semantics of epistemic
operators

C

Verification examples

(•)
R

(•)

((•))
D

C

(◦)
D

Conclusion

where((◦)) = {|n, X, (◦)|}R

This is “anonymous” because the counter run is equallypossible, so adversary is not sure whether A sent
something to B or C

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 7/23

Onion routing
actual run“counter” run
BA

Introduction((◦))

Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic

A

(◦)

B
((◦))

R
((•))

Semantics of epistemic
operators

R
(•)

C

Verification examples

(•)

((•))
D

C

(◦)
D

Conclusion

where((◦)) = {|n, X, (◦)|}R

Anonymity fails when:n private key of R is compromised
n we omit nonces, ((◦)) = {|X, (◦)|}Rn not enough padding, e.g. C is absent

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 7/23

Various “anonymity”
A number of proposals and objections...
Introduction
Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic
Semantics of epistemic

Anonymity, Unobservability, Pseudonymity, and Identity
Management – A Proposal for Terminology(Ongoing draft from July 2000)
http://dud.inf.tu-dresden.de/Literatur_V1.shtml

operators
Verification examples
Conclusion

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 8/23

Various “anonymity”
A number of proposals and objections...
Introduction
Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic
Semantics of epistemic

Anonymity, Unobservability, Pseudonymity, and Identity
Management – A Proposal for Terminology(Ongoing draft from July 2000)
http://dud.inf.tu-dresden.de/Literatur_V1.shtml

operators
Verification examples
Conclusion

With epistemic language we can formulate and verify
competing notions in a uniform manner! [Halpern, O’Neill]

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 8/23

Epistemic logic
A knows ϕ

2A ϕ
Introduction

3A ϕ

Example: onion routing(:=¬2A ¬ϕ)A suspects ϕ● Epistemic logic● “Anonymity” expressed withepistemic logic
Semantics of epistemic
operators
Verification examples
Conclusion

Semantics
W, {∼=A | A : agent}n W : set of possible worldsn ∼=A : observational equivalence for A

Internatinal Summer School Marktoberdorf¡¢

x |= 2A ϕ

⇐⇒

def

∀y ∼
=A x.

y |= ϕx |= 3A ϕ

⇐⇒

def

∃y ∼
=A x.

y |= ϕProvable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 9/23

“Anonymity” expressed with epistemic logic

Introduction

Sender anonymity
Given: B receives message (containing) m.
Weak ver.

Example: onion routing● Epistemic logic

Anonymity set {A1 , . . . , An }● “Anonymity” expressed withepistemic logic

A1

Semantics of epistemic
operators?
A m anonymizer

Verification examples
Conclusion

m B

?
m

..
.

anonymizer

m B

?
m

Not sure if A sent m

Internatinal Summer School Marktoberdorf

An
Each Ai is suspected as sender

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 10/23

“Anonymity” expressed with epistemic logic

Introduction

Sender anonymity
Given: B receives message (containing) m.
Weak ver.

Example: onion routing● Epistemic logic

Anonymity set {A1 , . . . , An }● “Anonymity” expressed withepistemic logic

A1

Semantics of epistemic
operators?
A m anonymizer

Verification examples
Conclusion

m B

?
m

..
.

anonymizer

m B

?
m

Not sure if A sent m¬2B A Sends mInternatinal Summer School Marktoberdorf

An
Each Ai is suspected as sender∧∧∧

3B A1 Sends m
3B A2 Sends m···
3B An Sends m

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 10/23

“Anonymity” expressed with epistemic logic
Unlinkability
Introduction

B

A

Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic

anonymizer

Semantics of epistemic
operators

C

Verification examples
Conclusion

D

Adversary is not sure if A sent something to B.

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 11/23

“Anonymity” expressed with epistemic logic
Unlinkability
Introduction

B

A

Example: onion routing● Epistemic logic● “Anonymity” expressed withepistemic logic

anonymizer

Semantics of epistemic
operators

C

Verification examples
Conclusion

D

Adversary is not sure if A sent something to B.
¬2spy ∃m. (A Sends m ∧ B Receives m)

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 11/23

“Anonymity” expressed with epistemic logic

Introduction
Example: onion routing

Plausible deniability
R can claim it is not aware of content m“I relayed something, but don’t know what it was!”● Epistemic logic● “Anonymity” expressed withepistemic logic
Semantics of epistemic

A

((m))

R

(m)

B

operators
Verification examples
Conclusion(m) = {|m|}B((m)) = {|n1 , B, (m)|}R

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 12/23

“Anonymity” expressed with epistemic logic

Introduction
Example: onion routing

Plausible deniability
R can claim it is not aware of content m“I relayed something, but don’t know what it was!”● Epistemic logic● “Anonymity” expressed withepistemic logic
Semantics of epistemic

A

((m))

R

(m)

B

operators
Verification examples
Conclusion(m) = {|m|}B((m)) = {|n1 , B, (m)|}R∀m. ¬2R (R Sends m)Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 12/23

Semantics of epistemic operators
Possible world = a run, or trace of protocol
Introduction
Example: onion routing
Semantics of epistemic
operators● Semantics of epistemic
operators● Reinterpretation of messages● Observational equivalence
Verification examples

Two aspects of observational equivalence ∼=A :n Not every event is observed by an agent(However we assume global eavesdropper as adversary)nConclusion

Internatinal Summer School Marktoberdorf

Use of cryptographic operation
Encryptions/hashes makes messages look random junk!
(Mauw, Verschuren, de Vink)

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 13/23

Semantics of epistemic operators
However, two random junks{|m|}A

Introduction
Example: onion routing
Semantics of epistemicand{|{|m|}A |}B

should be related.

operators● Semantics of epistemic
operators● Reinterpretation of messages● Observational equivalence
Verification examples

That is, mapping all undecryptable messages to single ⊥ is
not fine enough.

Conclusion

Our approach is finer than preceeding work, taking care ofthis point.

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 14/23

Reinterpretation of messages

Introduction

Our approach is finer, using reinterpretation
We cheat adversary, by reinterpretingmessage which looks
junk for adversary

Example: onion routing
Semantics of epistemic
operators● Semantics of epistemic
operators● Reinterpretation of messages

intoanother message

in the way adversary cannot detect a lie.

● Observational equivalence
Verification examples
Conclusion

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 15/23

Reinterpretation of messages

Introduction

Our approach is finer, using reinterpretation
We cheat adversary, by reinterpretingmessage which looks
junk for adversary

Example: onion routing
Semantics of epistemic
operators● Semantics of epistemic
operators● Reinterpretation of messages

intoanother message

in the way adversary cannot detect a lie.

● Observational equivalence
Verification examples
Conclusion

Definition U : a set of messages (e.g. spy’s possession)
Permutation π of messages is reinterpretation under U if:
π(p) = pπ({|m|}K ) = {|π(m)|}K
π(hash(m)) = hash(π(m))

for a primitive term p(
m, K ∈ U , or
if{|m|}K , K −1 ∈ U
if m ∈ U

π(hm1 , m2 i) = hπ(m1 ), π(m2 )i
In short, π preserves term structures available in U .
Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 15/23

Observational equivalence

Introduction

Definitionr∼=A r 0

Example: onion routing
Semantics of epistemic
operators

def⇐⇒● Semantics of epistemic∃π, reinterpretation under A’s possession, s.t.
π(r|A ) = r 0 |A

operators● Reinterpretation of messages● Observational equivalence
Verification examples
Conclusion

where r|A : A-visible part of rn For A 6= spy, r|A consists of events where A is sender or
receiver.
n r|spy = r, i.e., spy is a global eavesdropper.

∼=A is in fact an equivalence relation.
Hence 2A is S5-modality.

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 16/23

Observational equivalence
actual run
BA

Introduction((◦))

Example: onion routing“counter” run
A

(◦)

B
((◦))

R

Semantics of epistemic
operators((•))● Semantics of epistemic
operators● Reinterpretation of messages

C● Observational equivalence

(•)
R

(•)

((•))
D

C

(◦)
D

Verification examples
Conclusion

where

Internatinal Summer School Marktoberdorf((◦)) = {|n, (◦)|}Rn : random nonce

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 17/23

Observational equivalence
actual run
BA

Introduction((◦))

Example: onion routing“counter” run
A

∼
=spy

(◦)
R

Semantics of epistemic
operators((•))● Semantics of epistemic
operators● Reinterpretation of messages(•)

C● Observational equivalence

D

B
((◦))

(•)
R

((•))
C

(◦)
D

Verification examples
Conclusion

where((◦)) = {|n, (◦)|}R

Reinterpretation π:Internatinal Summer School Marktoberdorf

n : random nonce((◦)) 7→ ((◦))((•)) 7→ ((•))(◦) 7→ (•)(•) 7→ (◦)

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 17/23

Onion routing: unlinkability

Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples● Onion routing: unlinkability● Onion routing: plausible
deniability● Forgotten nonces





r=


A

···

((m))
R

···

Theorem

(m)

B







where
((m)) = {|n, B, (m)|}R

r |= ¬2spy ∃m. (A Sends m ∧ B Receives m)(A and B are unlinkable)● Private-key compromised● Other examples
Conclusion⇐⇒
some C 6= A sends ((m0 )) to R, before R relays (m).
(there is enough padding)
Proof [⇒] By contradiction. In ∀r 0 ∼=spy r, π of (m) must
result from π of ((m)). Hence they have same core ofonion.
Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 18/23

Onion routing: plausible deniability

Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples● Onion routing: unlinkability● Onion routing: plausible
deniability● Forgotten nonces





r=


A

···

((m))
R
(m)

···

B

Theorem For any m,● Private-key compromised







where
((m)) = {|n, B, (m)|}R

r |= ¬2R (R Sends m)● Other examples
Conclusion

Proof R doesn’t possess private-key of B, hencefor ∀m0 , ∃π: reinterpretation under R, which gives(actual run)Internatinal Summer School Marktoberdorf

∼
=R

A

((m0 ))

R

(m0 )

B

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 19/23

Flawed onion routing 1: forgotten nonces

Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples● Onion routing: unlinkability● Onion routing: plausible
deniability● Forgotten nonces

We forget nonces beneath skin of onion.


···
((m))
A




r=
R

(m)
···
B

where
((m)) = {|B, (m)|}R

Theorem Unlinkability fails, i.e.

● Private-key compromisedr |= 2spy ∃m. (A Sends m ∧ B Receives m)● Other examples
Conclusion

Proof Any reinterpretation π must be like(m) 7→ m1((m)) 7→ {|B, m1 |}R

since spy possesses public-key of R.
{|B, m1 |}R
m1
0 ∼
R
B,
A
Hence any r =spy r is liketherefore r 0 |= ∃m. (A Sends m ∧ B Receives m).
Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 20/23

Flawed OR 2: private-key compromised

Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples● Onion routing: unlinkability● Onion routing: plausible
deniability● Forgotten nonces

Private-key of R possessed by spy.


···
((m))
A




r=
R

(m)
···
B

where
((m)) = {|n, B, (m)|}R

Theorem Unlinkability fails, i.e.

● Private-key compromisedr |= 2spy ∃m. (A Sends m ∧ B Receives m)● Other examples
Conclusion

Proof Any reinterpretation π must be like(m) 7→ m1((m)) 7→ {|n, B, m1 |}RHence any r 0 ∼=spy r is like{|n, B, m1 |}Rm1R
B , thereforeA
r 0 |= ∃m. (A Sends m ∧ B Receives m).
Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 21/23

Other examples
n Can detect even more subtle (artificial) flaw in Onion
Introduction
Example: onion routing
Semantics of epistemic
operators

Routing: see full papern Crowds, for sender anonymityn Internet voting protocol RIESIn real use in the Netherlands (ongoing analysis)

Verification examples● Onion routing: unlinkability● Onion routing: plausible
deniability● Forgotten nonces● Private-key compromised● Other examples
Conclusion

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 22/23

Conclusionn Anonymity is important, hard to define, hard to verify
Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples
Conclusion● Conclusionn Competing notions are straightforwardly expressed withepistemic languagen First to consider use of cryptographic operations insemantics of epistemic logicn Finer treatment of cryptographic operations using
reinterpretationn Able to uniformly verify/falsify wide variety ofanonymizing systems
Future workn Justification of reinterpretation (cf. Abadi, Rogaway)n Tool supportn Quantitative analysis

Internatinal Summer School Marktoberdorf

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 23/23

Conclusionn Anonymity is important, hard to define, hard to verify
Introduction
Example: onion routing
Semantics of epistemic
operators
Verification examples
Conclusion● Conclusionn Competing notions are straightforwardly expressed withepistemic languagen First to consider use of cryptographic operations insemantics of epistemic logicn Finer treatment of cryptographic operations using
reinterpretationn Able to uniformly verify/falsify wide variety ofanonymizing systems
Future workn Justification of reinterpretation (cf. Abadi, Rogaway)n Tool supportn Quantitative analysis
Thank you for your attention!
Contact: Ichiro Hasuo www.sos.cs.ru.nl

Internatinal Summer School Marktoberdorf

ichiro@cs.ru.nl

Provable Anonymity – Ichiro Hasuo, Nijmegen, NL - p. 23/23