On Backward-Style Anonymity Verification

• KAWABE Yoshinobu

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

• MANO Ken

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

• SAKURADA Hideki

  NTT Communication Science Laboratories, NTT Corporation

• TSUKADA Yasuyuki

  NTT Communication Science Laboratories, NTT Corporation

Abstract

Many Internet services and protocols should guarantee anonymity; for example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an extension of the formulation of anonymity by Schneider and Sidiropoulos, this paper presents an inductive method based on backward anonymous simulations. We show that the existence of an image-finite backward anonymous simulation implies trace anonymity. We also demonstrate the anonymity verification of an e-voting protocol (the FOO protocol) with our backward anonymous simulation technique. When proving the trace anonymity, this paper employs a computer-assisted verification tool based on 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 (9), 2597-2606, 2008

  The Institute of Electronics, Information and Communication Engineers

Keywords

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

Details

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