Formal Approach to Anonymity and Privacy

Recent research shows that formal methods can play an important role in designing communications systems with rigorous anonymity and privacy requirements.

Electronic Voting Protocols: Target Examples

One of the formal definitions of the anonymity of a communications system is that a certain participant's specific action can be ``simulated'' by another arbitrary participant's corresponding action. Building on this definition, we have proposed an inductive method of proving anonymity [1], which can be applied to a system with an unbounded number of participants. Using this method, we have successfully proved the anonymity of the FOO electronic voting protocol (which was proposed by Fujioka, Okamoto, and Ohta in 1992) [2, 3]. Further, this method has been extended to formally prove the receipt-freeness of Lee et al.'s electronic voting protocol [4].

Duality of Anonymity and Privacy

We have also discussed anonymity and privacy in terms of a new fundamental concept called role interchangeability, which can be defined in the modal logic of knowledge. More specifically, we have treated privacy as a kind of ``dual'' of anonymity and have shown that exploiting this duality is useful for deriving anonymity and privacy from role interchangeability. We have also devised a method of proving role interchangeability, thereby demonstrating the voter anonymity and vote privacy of the FOO electronic voting protocol [5].

From Anonymity and Privacy toward Onymity and Identity

The idea of the duality between anonymity and privacy has been extended to consider the duality of onymity and identity. By this extension, we have revealed a logical structure underlying privacy-related information-hiding/disclosure properties [6, 7]. We have also discussed the relationships between our formulation and existing standard terminology, in particular Pfitzmann and Hansen's consolidated proposal [8].

Relevant References

[1] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, Theorem-proving anonymity of infinite-state systems, Information Processing Letters, Vol. 101, Issue 1 (January 2007) 46-51. [Abstract]

[2] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, Backward simulations for anonymity, in: D. Gollmann and J. Jürjens, editors, Sixth IFIP WG 1.7, GI FoMSESS Workshop on Issues in the Theory of Security (WITS '06) (March 2006) pp. 206-220. [Abstract]

[3] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, On backward-style anonymity verification, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E91-A, No. 9 (September 2008) 2597-2606. [Abstract]

[4] Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada, Theorem-proving receipt-freeness of an e-voting protocol (in Japanese), IPSJ Journal, Vol. 52, No. 9 (September 2011) 2549-2561. [Abstract]

[5] Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada, Role interchange for anonymity and privacy of voting, Journal of Logic and Computation, Vol. 20, Issue 6 (December 2010) 1251-1288. [Abstract]

[6] Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe, Anonymity, privacy, onymity, and identity: A modal logic approach, in: Proceedings of the 2009 IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09) (IEEE Computer Society Press, August 2009) pp. 42-51. [Abstract] [Slides (PDF)]

[7] Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe, Anonymity, privacy, onymity, and identity: A modal logic approach, Transactions on Data Privacy, Vol. 3, Issue 3 (December 2010) 177-198. [Abstract]

[8] Akiko Orita, Ken Mano, and Yasuyuki Tsukada, Translation of essential terms to Japanese, in: A. Pfitzmann and M. Hansen, A terminology for talking about privacy by data minimization: Anonymity, Unlinkability, Undetectability, Unobservability, Pseudonymity, and Identity Management, Version v0.34 (August 2010) pp. 74-78. [Anon Terminology Website]