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
相关论文
共 50 条
  • [1] Formalizing O notation in Isabelle/HOL
    Avigad, J
    Donnelly, K
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 357 - 371
  • [2] Formalizing rewriting introduction on Isabelle/HOL
    Kimura Y.
    Aoto T.
    Computer Software, 2020, 37 (02) : 104 - 119
  • [3] Formalizing IMO Problems and Solutions in Isabelle/HOL
    Maric, Filip
    Stojanovic-Durdevic, Sana
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (328): : 35 - 55
  • [4] Formalizing Graph Trail Properties in Isabelle/HOL
    Kovacs, Laura
    Lachnitt, Hanna
    Szeider, Stefan
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2020, 2020, 12236 : 190 - 205
  • [5] Formalizing Coppersmith's Method in Isabelle/HOL
    Kosaian, Katherine
    Tan, Yong Kiam
    Rozier, Kristin Yvonne
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2024, 2024, 14690 : 127 - 145
  • [6] Formalizing Jordan Normal Forms in Isabelle/HOL
    Thiemann, Rene
    Yamada, Akihisa
    PROCEEDINGS OF THE 5TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP'16), 2016, : 88 - 99
  • [7] Formalizing Pick's Theorem in Isabelle/HOL
    Binder, Sage
    Kosaian, Katherine
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2024, 2024, 14690 : 109 - 126
  • [8] Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
    From, Asta Halkjaer
    Eschen, Agnes Moesgard
    Villadsen, Jorgen
    INTELLIGENT COMPUTER MATHEMATICS (CICM 2021), 2021, 12833 : 32 - 46
  • [9] Formalizing Ordinal Partition Relations Using Isabelle/HOL
    Dzamonja, Mirna
    Koutsoukou-Argyraki, Angeliki
    Paulson, Lawrence C.
    EXPERIMENTAL MATHEMATICS, 2022, 31 (02) : 383 - 400
  • [10] Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL
    Hess, Andreas Viktor
    Modersheim, Sebastian
    2017 IEEE 30TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2017, : 451 - 463
12345