On Backward-Style Anonymity Verification
スポンサーリンク
概要
- 論文の詳細を見る
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.
- (社)電子情報通信学会の論文
- 2008-09-01
著者
-
Kawabe Yoshinobu
Ntt Corp. Atsugi‐shi Jpn
-
Kawabe Yoshinobu
Ntt Communication Science Laboratories Ntt Corporation
-
Sakurada Hideki
Ntt Corp. Atsugi‐shi Jpn
-
Mano Ken
NTT Communication Science Labs.
-
Mano Ken
Ntt Communication Science Laboratories
-
Sakurada Hideki
Ntt Communication Science Laboratories Ntt Corporation
-
TSUKADA Yasuyuki
NTT Communication Science Laboratories, NTT Corporation
-
Tsukada Yasuyuki
Ntt Communication Science Laboratories Ntt Corporation
関連論文
- A new proof of Chew's theorem(Theory of Rewriting Systems and Its Applications)
- 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
- A Metric Semantics for the $\pi$-Calculus Extended with External Events(Concurrency Theory and Applications '96)
- 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