Formalizing provable anonymity in Isabelle/HOL

被引：4

作者：

Li, Yongjian ^{[1
,2
]}

Pang, Jun ^{[3
,4
]}

机构：

[1] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China

[2] Capital Normal Univ, Coll Informat Engn, Beijing, Peoples R China

[3] Univ Luxembourg, Fac Sci Technol & Commun, Walferdange, Luxembourg

[4] Univ Luxembourg, Interdisciplinary Ctr Secur Reliabil & Trust, Walferdange, Luxembourg

来源：

FORMAL ASPECTS OF COMPUTING | 2015年 / 27卷 / 02期

基金：

中国国家自然科学基金;

关键词：

Anonymity; Security protocols; Theorem proving; Inductive methods; PROTOCOL; SECURITY; VERIFICATION; FRAMEWORK; CONES; FOCI;

D O I：

10.1007/s00165-014-0315-x

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We formalize in a theorem prover the notion of provable anonymity. Our formalization relies on inductive definitions of message distinguishing ability and observational equivalence on traces observed by the intruder. Our theory differs from its original proposal and essentially boils down to the inductive definition of distinguishing messages with respect to a knowledge set for the intruder. We build our theory in Isabelle/HOL to achieve a mechanical framework for the analysis of anonymity protocols. Its feasibility is illustrated through two case studies of the Crowds and Onion Routing protocols.

引用

页码：255 / 282

页数：28