An Adversary Model for Simulation-Based Anonymity Proof

• KAWABE Yoshinobu

  NTT Communication Science Laboratories, NTT Corporation The Institute of Electronics, Information and Communication Engineers

• SAKURADA Hideki

  NTT Communication Science Laboratories, NTT Corporation

Abstract

The use of a formal method is a promising approach to developing reliable computer programs. This paper presents a formal method for anonymity, which is an important security property of communication protocols with regard to a user's identity. When verifying the anonymity of security protocols, we need to consider the presence of adversaries. To formalize stronger adversaries, we introduce an adversary model for simulation-based anonymity proof. This paper also demonstrates the formal verification of a communication protocol. We employ Crowds, which is an implementation of an anonymous router, and verify its anonymity. After describing Crowds in a formal specification language, we prove its anonymity with a theorem prover.

Journal

• IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

  IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences E91-A (4), 1112-1120, 2008

  The Institute of Electronics, Information and Communication Engineers

Keywords

• formal methods
• anonymity
• software security
• verification
• theorem-proving

Details

• CRID: 1390282681287779840
• NII Article ID: 10026848731
• NII Book ID: AA10826239
• DOI: 10.1093/ietfec/e91-a.4.1112
• ISSN: 17451337
• ISSN: 09168508
• Web Site: https://www.jstage.jst.go.jp/article/transfun/E91.A/4/E91.A_4_1112/_pdf
• Text Lang: en
• Data Source:
  • JaLC
  • Crossref
  • CiNii Articles
• Abstract License Flag: Disallowed