an inductive approach to provable anonymity

ISCAS OpenIR

	an inductive approach to provable anonymity
	Li Yongjian; Pang Jun
	2011
会议名称	2011 6th International Conference on Availability, Reliability and Security, ARES 2011
会议录名称	Proceedings of the 2011 6th International Conference on Availability, Reliability and Security, ARES 2011
页码	454-459
会议日期	August 22,
会议地点	Vienna, Austria
收录类别	EI
ISBN	9780769544854
部门归属	(1) State Key Laboratory of Computer Sciences Institute of Software Chinese Academy of Sciences China; (2) Computer Science and Communications University of Luxembourg Luxembourg
摘要	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. © 2011 IEEE.; 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. © 2011 IEEE.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16229
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Li Yongjian,Pang Jun. an inductive approach to provable anonymity[C],2011:454-459.