An Adversary Model for Simulation-Based Anonymity Proof

スポンサーリンク

概要

• 論文の詳細を見る

• 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 users 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.

• （社）電子情報通信学会の論文
• 2008-04-01

著者

• Kawabe Yoshinobu

  Ntt Corp. Atsugi‐shi Jpn

• Kawabe Yoshinobu

  Ntt Communication Science Laboratories Ntt Corporation

• Sakurada Hideki

  Ntt Corp. Atsugi‐shi Jpn

• Sakurada Hideki

  Ntt Communication Science Laboratories Ntt Corporation

関連論文

• Termination of Order-Sorted Rewriting with Non-minimal Signatures
• Name Creation Implements Restriction in the π-Calculus
• On Backward-Style Anonymity Verification
• An Adversary Model for Simulation-Based Anonymity Proof
• Verifying Trace Equivalence of a Shared-Memory-Style Communication System(Selected Papers from the 17th Workshop on Circuits and Systems in Karuizawa)
• Modularity of Confluence in Order-Sorted Term Rewriting Systems

スポンサーリンク