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
相关论文
共 33 条
[31]   Provable secure authentication protocol with anonymity for roaming service in global mobility networks [J].
Zhou, Tao ;
Xu, Jing .
COMPUTER NETWORKS, 2011, 55 (01) :205-213
[32]   An improved and provable remote user authentication scheme based on elliptic curve cryptosystem with user anonymity [J].
Xu, Lili ;
Wu, Fan .
SECURITY AND COMMUNICATION NETWORKS, 2015, 8 (02) :245-260
[33]   A Provable One-way Authentication Key Agreement Scheme with User Anonymity for Multi-server Environment [J].
Zhu, Hongfeng .
KSII TRANSACTIONS ON INTERNET AND INFORMATION SYSTEMS, 2015, 9 (02) :811-829
1234