DocumentCode
1832941
Title
An Inductive Approach to Provable Anonymity
Author
Li, Yongjian ; Pang, Jun
Author_Institution
State Key Lab. of Comput. Sci., Inst. of Software, Beijing, China
fYear
2011
fDate
22-26 Aug. 2011
Firstpage
454
Lastpage
459
Abstract
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.
Keywords
Internet; message authentication; routing protocols; theorem proving; Isabelle/HOL; anonymity protocols; inductive approach; inductive definitions; message distinguish ability; observational equivalence; onion routing protocol; provable anonymity; theorem prover; Cryptography; Diamond-like carbon; Knowledge engineering; Receivers; Routing protocols; Servers; Inductive Approach; Isabelle; Provable Anonymity; anonymity; onion protocol;
fLanguage
English
Publisher
ieee
Conference_Titel
Availability, Reliability and Security (ARES), 2011 Sixth International Conference on
Conference_Location
Vienna
Print_ISBN
978-1-4577-0979-1
Electronic_ISBN
978-0-7695-4485-4
Type
conf
DOI
10.1109/ARES.2011.70
Filename
6046000
Link To Document