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 条

[21] A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL [J].

Kosaian, Katherine ;

Tan, Yong Kiam ;

Platzer, Andre .

PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023, 2023, :211-224

[22] Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation [J].

Wang, Haitao ;

Song, Lihua .

IEEE ACCESS, 2021, 9 :25002-25013

[23] Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL [J].

Foster, Simon ;

Hur, Chung-kil ;

Woodcock, Jim .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2025, 34 (04) :1-40

[24] Programming and verifying a declarative first-order prover in Isabelle/HOL [J].

Jensen, Alexander Birch ;

Larsen, John Bruntse ;

Schlichtkrull, Anders ;

Villadsen, Jorgen .

AI COMMUNICATIONS, 2018, 31 (03) :281-299

[25] A new method of formalizing anonymity based on protocol composition logic [J].

Feng, Tao ;

Han, Shining ;

Guo, Xian ;

Ma, Donglin .

SECURITY AND COMMUNICATION NETWORKS, 2015, 8 (06) :1132-1140

[26] Formalizing Anonymity-Delay Tradeoffs in Smart Grid Networks [J].

Lipton, Benjamin ;

Mishra, Sumita .

2016 THE 4TH IEEE INTERNATIONAL CONFERENCE ON SMART ENERGY GRID ENGINEERING (SEGE), 2016, :353-357

[27] A formal proof of Sylow's theorem -: An experiment in abstract algebra with Isabelle HOL [J].

Kammüller, F ;

Paulson, LC .

JOURNAL OF AUTOMATED REASONING, 1999, 23 (3-4) :235-264

[28] Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem [J].

Li, Wenda ;

Paulson, Lawrence C. .

PROCEEDINGS OF THE 8TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP' 19), 2019, :52-64

[29] Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL [J].

Dalvandi, Sadegh ;

Dongol, Brijesh ;

Doherty, Simon ;

Wehrheim, Heike .

JOURNAL OF AUTOMATED REASONING, 2022, 66 (01) :141-171

[30] An Efficient Identity Authentication Scheme With Provable Security and Anonymity for Mobile Edge Computing [J].

Xu, Yuan ;

Zhou, Yanwei ;

Yang, Bo ;

Qiao, Zirui ;

Wang, Zhaolong ;

Xia, Zhe ;

Zhang, Mingwu .

IEEE SYSTEMS JOURNAL, 2023, 17 (01) :1012-1023

← 1 2 3 4 →