Sciweavers

ARESEC
2011

An Inductive Approach to Provable Anonymity

12 years 3 months ago
An Inductive Approach to Provable Anonymity
—We formalise in a theorem prover the notion of provable anonymity proposed by Garcia et al. Our formalization relies on inductive definitions of message distinguish ability and observational equivalence over observed traces by the intruder. Our theory differs from its original proposal which essentially boils down to the existence of a reinterpretation function. We build our theory in Isabelle/HOL to have a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through the onion routing protocol.
Yongjian Li, Jun Pang
Added 12 Dec 2011
Updated 12 Dec 2011
Type Journal
Year 2011
Where ARESEC
Authors Yongjian Li, Jun Pang
Comments (0)