Probabilistic Anonymity via
Coalgebraic Simulations
Ichiro Hasuo
Radboud Universiteit Nijmegen, the Netherlands(From 2007.5, also at: RIMS, Kyoto Univ., Japan)

Japanese “FranceTelecom”

Joint work with Yoshinobu Kawabe
NTT Communication Science Laboratories, Japan

Online privacy
Online anonymity
is attracting growingz Threatsz ISPs in EU are forced to keep logs of your web accessz Your passport stores your fingerprint on a RFID chipz Public concernsz Research interestz See Anonymity Bibliography
http://freehaven.net/anonbib/
zThe field is quite youngz Compared to “traditional” security notions such as
secrecy, authentication

Overview:
Probabilistic anonymity via coalgebraic simulations

Simulation-based proof method fornon-deterministic = possibilistic
anonymity [KawabeMST06]
Generic, coalgebraic theory of
traces and simulations[IH,Jacobs,Sokolova]•non-det. Î prob. is just a change of aparameter

Simulation-based proof method forprobabilisticanonymity

For you to take homez

Probability in anonymity
z Subtlety in definition of “probabilistic anonymity”zPower of categorical methods in computer sciencez Specifically, theory of coalgebrasz Abstraction and genericityz Category theory in action!

References
Coalgebraic theory of traces and simulations

zzz

Ichiro Hasuo, Bart Jacobs and Ana Sokolova
Generic Trace Theory
CMCS’06, ENTCS 164
Ichiro Hasuo
Generic Forward and Backward Simulations
CONCUR 2006, LNCS 4137

Y. Kawabe

B. Jacobs

Simulation-based proof method of anonymityzz

Y. Kawabe, K. Mano, H. Sakurada and Y. Tsukada
Theorem-proving anonymity of infinite state systems
Information Processing Letters, to appear

zY. Kawabe, K. Mano, H. Sakurada and Y. Tsukada
Backward simulations for anonymity
WITS’06zIchiro Hasuo and Yoshinobu Kawabe
Probabilistic Anonymity via Coalgebraic Simulations
ESOP’07, to appear

A. Sokolova

Nina HagenPart I:
Non-deterministic version of∃ simulation Î anonymityNon-deterministic “trace” anonymity[Schneider&Sidiropoulos,ESORICS’96]

Anonymous donation as an example
Anonymous!

Not anonymous!

Are these protocols “anonymous”?
Definition (Trace anonymity)X

is anonymous ⇔•Ana : actor action(invisible foradversary)•$5: observable action

Observation
can be attributed toanybody

Non-deterministic(∃ simulation Î anonymity)[Kawabe,Mano,Sakurada,Tsukada 2006]

An automaton whichmodels ananonymizing protocol

Theorem∃ forward/backward simulation from an(X) to X
Î X is anonymousz

Theory of traces and simulationsz

Forward simulation R issuch that:z

Backward simulation R
is such that:z

Soundness theorem:∃ fwd/bwd simulation Î trace inclusion[Lynch&Vaandrager, Inf.&Comp. 1995]zNon-deterministic(∃ simulation Î anonymity)[Kawabe,Mano,Sakurada,Tsukada 2006]

Theorem∃ forward/backward simulation from an(X) to XÎ X is anonymous“anonymized” version of X(trivially anonymous)

Proof.
X is anonymousÍ tr(X) = tr(an(X))Í tr(X) ⊇ tr(an(X))Í ∃ simulation from an(X) to X

(anonymity is trace-based)(⊆ is trivial)(soundness theorem!)Part II:
Probabilistic anonymity and(∃ simulation Î anonymity)

Probabilistic anonymity

Anonymous!
zz“Anonymous”!

Not anonymous!

Are these protocols “anonymous”?
These are all anonymous in a possibilistic sense.
Î definition of “probabilistic anonymity”?

Probabilistic anonymity[Bhargava&Palamidessi, CONCUR’05]

Definition (Probabilistic anonymity)
X is anonymous

such as 〈 $5 〉⇔conditional probability

More on probabilistic anonymity
Definition (Probabilistic anonymity)
X is anonymous ⇔z

Intuition:“Observation ofdonating”

does not carry any info. on who isz

A priori distribution of suspicion need not be uniformzHowever, after any observation, any agent must be exactly
as suspicious as before

More on probabilistic anonymity

I Know Bart is more
likely to donate

I Know Bart is more
likely to donate

More on probabilistic anonymity$10K

Someone donated $10K,
which is more likely
by Bart (as Isuspected)…
(anonymous)$10K

Bart wouldn’t donate
such an amount.
This time it’s likelythat Ana did!
(not anonymous)

Again the same scenario:(∃ simulation Î anonymity)

probabilistic
automaton

Theorem∃ forward/backward simulation from an(X) to X
Î X is anonymous
Can we do thisprobabilistically?
• What is an(X)?

Proof.

probabilistic anonymity

X is anonymous

trace distribution

Í tr(X) = tr(an(X))Í tr(X) ⊇ tr(an(X))• What is“probabilisticsimulation”?

(anonymity is trace-based)probabilistic simulation(⊆ is trivial)Í ∃ simulation from an(X) to X

(soundness theorem!)an(X), in a probabilistic settingz

Idea: distribute probability according to a-priori suspicion

zA-priori suspicion:HenceAgain the same scenario:(∃ simulation Î anonymity)

probabilistic
automaton

Theorem∃ forward/backward simulation from an(X) to X
Î X is anonymous
Can we do thisprobabilistically?
• What is an(X)?

Proof.

probabilistic anonymity

X is anonymous

trace distribution

Í tr(X) = tr(an(X))Í tr(X) ⊇ tr(an(X))• What is“probabilisticsimulation”?

(anonymity is trace-based)probabilistic simulation(⊆ is trivial)Í ∃ simulation from an(X) to X

(soundness theorem!)Intermezzo:
Coalgebraic theory oftraces and simulations

Theory of coalgebraszCategorical theory of “state-based systems”
Everything as objects and arrowsz•

Focus on “essence”•Abstraction, genericity

Base categories
z Sets Î theory of bisimilarity [Rutten,TCS’00]
z Kl(T) Î theory of traces and simulations[IH,Jacobs,Sokolova,CMCS’06][IH,CONCUR’06]

Traces and simulations,Parameter F :coalgebraicallyfor transition-type
Systema coalgebra

Tracesemantics

inParameter T :for branching-type

Simulations

forward sim.

backward sim.

General soundness theorem : ∃ simulation Î trace incl.

Genericity

T and FBy changing parameters, the framework coverszdifferent branching-types by different T
We exploit this!
z non-determinism• Anything we can do in az probabilistic branching
non-det. setting,z• we can also do in adifferent transition-types by different
F
probabilistic settingz LTS:x a (a,x’)
z Context-free grammar: x a 〈 “¬”, x 〉x a 〈 x, “∧”, x 〉F: a functor
for transition-type

Systems as coalgebras
A system is:in
T: a monadfor branching-typez T is a monad, for branching-type. Examples:z P , powerset monadz

for non-determinism

z D , subdistribution monadzfor (generative) probabilistic branchingSystems as coalgebras
A system is:

A category wherebranching is implicitin, a function: the Kleisli category for Tz Main point:
for T = P,Parametersin

A system is:, a function

branching-type:non-determinismz

T = P,

F=1+Σ×-transition-type:terminate or (output, next)

such asLTS with explicit termination

Parameters
A system is:in, a functionz

T = P,

F=1+Σ×-LTS with explicit terminationz

T = D,

F=1+Σ×-

Generative probabilistic systemz

T = P,F = ( Σ + - )*Context-free grammar

Trace semantics[IH, Jacobs, Sokolova. CMCS’06]

1.

∃ final coalgebra

For any system

2.

in,

∃! f such that

This induced f gives (finite) trace semantics

Forward simulation

Take T=Pin
R : a relation, because

Forward simulationHence

implies

Backward simulation

Henceimplies

Main result:general soundness theorem∃ forward/backward simulation
trace inclusion
Proof.

inz

Also completeness result, as easily

Summary:
we have illustrated
SystemTracesemantics

inSimulations

forward sim.

backward sim.

General soundness theorem : ∃ simulation Î trace incl.

Back to probabilistic anonymity

Back to probabilistic
anonymity

probabilistic
automaton

Theorem∃ forward/backward simulation from an(X) to X
Î X is anonymous
Can we do thisprobabilistically?
• What is an(X)?

Proof.

probabilistic anonymity

X is anonymous

trace distribution

Í tr(X) = tr(an(X))Í tr(X) ⊇ tr(an(X))• What is“probabilisticsimulation”?

(anonymity is trace-based)probabilistic simulation(⊆ is trivial)Í ∃ simulation from an(X) to X

(soundness theorem!)Probabilistic simulation
via coalgebraic simulationf : fwd simulation from Y to X⇔
in⇔Coalgebra for•T = D (prob. branching)•F = A ×{}+A× _Soundness comes for freeby

Probabilistic(∃ simulation Î anonymity)[IH&Kawabe,2006]

Theorem∃ forward/backward simulation from an(X) to X
Probabilistic
Î X is anonymous
Probabilistically
Proof.
X is anonymousÍ tr(X) = tr(an(X))(anonymity is trace-based)Í tr(X) ⊇ tr(an(X))(⊆ is by constr. of an(X))Í ∃ simulation from an(X) to X

(soundness theorem!)Probabilistic(∃ simulation Î anonymity)[IH&Kawabe,2006]

Theorem∃ forward/backward simulation from an(X) to X
Probabilistic
Î X is anonymous
Probabilisticallyz

Should be useful in theorem-proving anonymityz

This is the case in a non-deterministic settingz Verification of the FOO voting protocol[Kawabe,Mano,Sakurada,Tsukada’06]

zProbabilistic verification example is yet to be foundz Currently our running example is dining cryptographers[Chaum’88]

Conclusion
non-deterministic (∃ simulation Î anonymity)[KawabeMST06]

Generic, coalgebraic theory oftraces and simulations [IH,Jacobs,Sokolova]• T = P Î non-determinism• T = D Î probability

probabilistic (∃ simulation Î anonymity)[Current work]

Conclusion and future workz

Future work
zBigger verification example?
zSystems with both non-determinism and probability?
z As in [Segala&Lynch’95]
z Important also for anonymity applications [Palamidessi,MFPS’05]
z Suitable coalgebraic framework is missing

zWeaker notion of anonymity?
z Current “anonymity” notion is pretty strongz “Simulation-based” method also for weaker notions?

For you to take home:Thank you for yourattention!

• Probability in anonymity

Ichiro Hasuo, U. Nijmegen, NL• Category theory in action!

http://www.cs.ru.nl/~ichiro