On Backward-Style Anonymity Verification

Yoshinobu KAWABE; Ken MANO; Hideki SAKURADA; Yasuyuki TSUKADA

doi:10.1093/ietfec/e91-a.9.2597

On Backward-Style Anonymity Verification

Yoshinobu KAWABE, Ken MANO, Hideki SAKURADA, Yasuyuki TSUKADA

Full Text Views

0

Cite this

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.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E91-A No.9 pp.2597-2606

Publication Date: 2008/09/01

Publicized

Online ISSN: 1745-1337

DOI: 10.1093/ietfec/e91-a.9.2597

Type of Manuscript: PAPER

Category: Cryptography and Information Security

Cite this

Copy

Yoshinobu KAWABE, Ken MANO, Hideki SAKURADA, Yasuyuki TSUKADA, "On Backward-Style Anonymity Verification" in IEICE TRANSACTIONS on Fundamentals, vol. E91-A, no. 9, pp. 2597-2606, September 2008, doi: 10.1093/ietfec/e91-a.9.2597.
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.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e91-a.9.2597/_p

Copy

@ARTICLE{e91-a_9_2597,
author={Yoshinobu KAWABE, Ken MANO, Hideki SAKURADA, Yasuyuki TSUKADA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={On Backward-Style Anonymity Verification},
year={2008},
volume={E91-A},
number={9},
pages={2597-2606},
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.},
keywords={},
doi={10.1093/ietfec/e91-a.9.2597},
ISSN={1745-1337},
month={September},}

Copy

TY - JOUR
TI - On Backward-Style Anonymity Verification
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 2597
EP - 2606
AU - Yoshinobu KAWABE
AU - Ken MANO
AU - Hideki SAKURADA
AU - Yasuyuki TSUKADA
PY - 2008
DO - 10.1093/ietfec/e91-a.9.2597
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E91-A
IS - 9
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - September 2008
AB - 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.
ER -