On Backward-Style Anonymity Verification

Yoshinobu KAWABE  Ken MANO  Hideki SAKURADA  Yasuyuki TSUKADA  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E91-A   No.9   pp.2597-2606
Publication Date: 2008/09/01
Online ISSN: 1745-1337
DOI: 10.1093/ietfec/e91-a.9.2597
Print ISSN: 0916-8508
Type of Manuscript: PAPER
Category: Cryptography and Information Security
Keyword: 
formal methods,  anonymity,  software security,  verification,  theorem-proving,  

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




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