An Adversary Model for Simulation-Based Anonymity Proof

Yoshinobu KAWABE  Hideki SAKURADA  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E91-A   No.4   pp.1112-1120
Publication Date: 2008/04/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e91-a.4.1112
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)
Category: 
Keyword: 
formal methods,  anonymity,  software security,  verification,  theorem-proving,  

Full Text: PDF(209.4KB)>>
Buy this Article




Summary: 
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.