For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
An Adversary Model for Simulation-Based Anonymity Proof
Yoshinobu KAWABE Hideki SAKURADA
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2008/04/01
Online ISSN: 1745-1337
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Selected Papers from the 20th Workshop on Circuits and Systems in Karuizawa)
formal methods, anonymity, software security, verification, theorem-proving,
Full Text: PDF(209.4KB)>>
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.