Group Anonymity in Security Protocols
Ferucio Laurenţiu Ţiplea, Cosmin Vârlan
DOI: http://dx.doi.org/10.15439/2018F43
Citation: Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 15, pages 407–416 (2018)
Abstract. Group anonymity, as an instance of information hiding, means that an agent is not identifiable within a group of agents with respect to an observer. In this paper we define group anonymity in security protocols by taking into account two types of observers: honest agents, as local observers of the protocol execution, and intruders (active or passive), as global observers of the protocol execution. It is shown that an action may be group anonymous in a protocol under a passive intruder but not in the same protocol under an active intruder, and vice versa. In case of basic-term actions, group anonymity in a protocol under an active intruder implies group anonymity in the same protocol under a passive intruder. A broad spectrum of relationships between group anonymity for various types of actions is developed, as well as relationships between group anonymity, minimal anonymity, and role interchangeability. Finally, the decidability and complexity status of the decision problems induced by these concepts is completely discussed. Thus, it is shown that group anonymity and role interchangeability are undecidable in unrestricted protocols. Group anonymity is complete for NEXPTIME when it is restricted to basic-term actions and bounded security protocols, and it is complete for NP when it is restricted to basic-term actions and 1-session bounded security protocols.
References
- D. Chaum, “Untraceable electronic mail, return addresses, and digital pseudonyms,” Communications of the ACM, vol. 24, no. 2, pp. 84–88, Feb 1981. http://dx.doi.org/10.1145/358549.358563. [Online]. Available: http://dx.doi.org/10.1145/358549.358563
- D. Chaum, “Security without identification: Transaction systems to make big brother obsolete,” Communications of the ACM, vol. 28, no. 10, pp. 1030–1044, Oct 1985. http://dx.doi.org/10.1145/4372.4373. [Online]. Available: http://dx.doi.org/10.1145/4372.4373
- D. Chaum, “The dining cryptographers problem: Unconditional sender untraceability,” Journal of Cryptology, vol. 1, no. 1, pp. 65–76, 1988. http://dx.doi.org/10.1007/BF00206326. [Online]. Available: http://dx.doi.org/10.1007/BF00206326
- S. Schneider and A. Sidiropoulos, “CSP and anonymity.” in 4th European Symposium on Research in Computer Security (ESORICS’96), ser. Lecture Notes in Computer Science, E. Bertino, H. Kurth, G. Martella, and E. Montolivo, Eds., no. 1146, 1996. http://dx.doi.org/10.1007/3-540-61770-1 38 pp. 198–218. [Online]. Available: http://dx.doi.org/10.1007/3-540-61770-1 38
- M. K. Reiter and A. D. Rubin, “Crowds: Anonymity for web transactions,” ACM Trans. Inf. Syst. Secur., vol. 1, pp. 66–92, Nov 1998. http://dx.doi.org/10.1145/290163.290168. [Online]. Available: http://dx.doi.org/10.1145/290163.290168
- P. F. Syverson and S. G. Stubblebine, “Group principals and the formalization of anonymity,” in World Congress on Formal Methods’99, 1999. http://dx.doi.org/10.1007/3-540-48119-2 45 pp. 814–833. [Online]. Available: http://dx.doi.org/10.1007/3-540-48119-2 45
- R. Dingledine, N. Mathewson, and P. Syverson, “Tor: The second-generation onion router,” In 13th USENIX Security Symposium, 2004.
- D. Hughes and V. Shmatikov, “Information hiding, anonymity and privacy: A modular approach,” Journal of Computer Security, vol. 12, pp. 3–36, Jan 2004. http://dx.doi.org/10.3233/JCS-2004-12102. [Online]. Available: http://dx.doi.org/10.3233/JCS-2004-12102
- S. Mauw, J. Verschuren, and E. P. de Vink, “A formalization of anonymity and onion routing,” in In Proceedings of the 9th European Symposium on Research in Computer Security (ESORICS 2004). Springer, 2004. http://dx.doi.org/10.1007/978-3-540-30108-0_7 pp. 109–124.
- F. D. Garcia, I. Hasuo, W. Pieters, and P. van Rossum, “Provable anonymity,” in Proceedings of the 2005 ACM Workshop on Formal Methods in Security Engineering (FMSE’05), 2005. http://dx.doi.org/10.1145/1103576.1103585 pp. 63–72. [Online]. Available: http://dx.doi.org/10.1145/1103576.1103585
- J. Y. Halpern and K. R. O’Neill, “Anonymity and information hiding in multi-agent systems,” Journal of Computer Security, vol. 13, no. 3, pp. 483–514, 2005. http://dx.doi.org/10.1109/CSFW.2003.1212706.
- K. Mano, Y. Kawabe, H. Sakurada, and Y. Tsukada, “Role interchangebility and verification of electronic voting,” in The 2006 Symposium on Cryptography and Information Security, Hiroshima, Japan, Jan 2006.
- T. Chothia, S. Orzan, J. Pang, and M. T. Dashti, “A framework for automatically checking anonymity with μcrl,” in In Proceedings TGC06, LNCS, 2007. http://dx.doi.org/10.1007/978-3-540-75336-0 19 pp. 301–318. [Online]. Available: http://dx.doi.org/10.1007/978-3-540-75336-0 19
- J. Feigenbaum, A. Johnson, and P. Syverson, “A model of onion routing with provable anonymity,” in In Proceedings of the 11th Financial Cryptography and Data Security Conference. Springer-Verlag, 2007. http://dx.doi.org/10.1007/978-3-540-77366-5 9 pp. 57–71. [Online]. Available: http://dx.doi.org/10.1007/978-3-540-77366-5 9
- Y. Kawabe, K. Mano, H. Sakurada, and Y. Tsukada, “Theorem-proving anonymity of infinite-state systems,” Inf. Process. Lett., vol. 101, pp. 46–51, Jan 2007. http://dx.doi.org/10.1016/j.ipl.2006.06.016. [Online]. Available: http://dx.doi.org/10.1016/j.ipl.2006.06.016
- X. Sun, H. Wang, and J. Li, “On the complexity of restricted k-anonymity problem,” in Proceedings of the 10th Asia-Pacific Web Conference on Progress in WWW Research and Development, ser. APWeb’08. Berlin, Heidelberg: Springer-Verlag, 2008. ISBN 3-540-78848-4, 978-3-540-78848-5 pp. 287–296.
- M. Edman and B. Yener, “On anonymity in an electronic society: A survey of anonymous communication systems,” ACM Computing Surveys, vol. 42, no. 1, 2009. http://dx.doi.org/10.1145/1592451.1592456. [Online]. Available: http://dx.doi.org/10.1145/1592451.1592456
- J. F. Groote and S. Orzan, “Parameterised anonymity,” in Formal Aspects in Security and Trust, P. Degano, J. Guttman, and F. Martinelli, Eds. Berlin, Heidelberg: Springer-Verlag, 2009, pp. 177–191. ISBN 978-3-642-01464-2. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-01465-9 12
- H. Comon-Lundh, Y. Kawamoto, and H. Sakurada, “Computational and symbolic anonymity in an unbounded network,” JSIAM Letters, vol. 1, pp. 28–31, 2009. http://dx.doi.org/10.14495/jsiaml.1.28. [Online]. Available: http://dx.doi.org/10.14495/jsiaml.1.28
- Y. Tsukada, K. Mano, H. Sakurada, and Y. Kawabe, “Anonymity, privacy, onymity, and identity: A modal logic approach,” in 2009 International Conference on Computational Science and Engineering, 2009. http://dx.doi.org/10.1109/CSE.2009.251 pp. 42–51. [Online]. Available: http://dx.doi.org/0.1109/CSE.2009.251
- C. A. Ardagna, S. Jajodia, P. Samarati, and A. Stavrou, “Providing mobile users’ anonymity in hybrid networks,” in European Symposium on Research in Computer Security (ESORICS 2010), ser. Lecture Notes in Computer Science, D. Gritzalis, B. Preneel, and T. Theoharidou, Eds., vol. 6345, 2010. http://dx.doi.org/10.1007/978-3-642-15497-3_33 pp. 540–557. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-15497-3_33
- M. Backes, G. Doychev, M. Dürmuth, and B. Köpf, “Speaker recognition in encrypted voice streams,” in European Symposium on Research in Computer Security (ESORICS 2010), ser. Lecture Notes in Computer Science, D. Gritzalis, B. Preneel, and T. Theoharidou, Eds., vol. 6345, 2010. http://dx.doi.org/10.1007/978-3-642-15497-3 31 pp. 508–523. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-15497-3 31
- A. Pfitzmann and M. Hansen, “A terminology for talking about privacy by data minimization: Anonymity, unlinkability, undetectability, unobservability, pseudonymity, and identity management,” http://dud.inf.tu-dresden.de/literatur/Anon_Terminology_v0.34.pdf, Aug 2010.
- F. L. Ţiplea, L. Vamanu, and C. Vârlan, “Complexity of anonymity for security protocols,” in European Symposium on Research in Computer Security (ESORICS 2010), ser. Lecture Notes in Computer Science, D. Gritzalis, B. Preneel, and T. Theoharidou, Eds., vol. 6345, 2010. http://dx.doi.org/10.1007/978-3-642-15497-3 34 pp. 558–572. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-15497-3 34
- I. Goriac, “An epistemic logic based framework for reasoning about information hiding,” in Availability, Reliability and Security, International Conference on. Los Alamitos, CA, USA: IEEE Computer Society, 2011. http://dx.doi.org/10.1109/ARES.2011.49 pp. 286–293. [Online]. Available: http://dx.doi.org/10.1109/ARES.2011.49
- F. L. Ţiplea, L. Vamanu, and C. Vârlan, “Reasoning about minimal anonymity in security protocols,” Future Generation Computer Systems, vol. 29, pp. 828–842, March 2013. http://dx.doi.org/10.1016/j.future.2012.02.001. [Online]. Available: http://dx.doi.org/10.1016/j.future.2012.02.001
- S. Kramer, “Cryptographic protocol logic: Satisfaction for (timed) Dolev-Yao cryptography,” The Journal of Logic and Algebraic Programming, vol. 77, pp. 60–91, Sep 2008. http://dx.doi.org/10.1016/j.jlap.2008.05.005. [Online]. Available: http://dx.doi.org/10.1016/j.jlap.2008.05.005
- R. Ramanujam and S. P. Suresh, “A decidable subclass of unbounded security protocols,” in Workshop on Issues in the Theory of Security (WITS’03), 2003, pp. 11–20.
- F. L. Ţiplea, C. Enea, and C. V. Bı̂rjoveanu, “Decidability and complexity results for security protocols,” in Verfication of Infinite-state Systems with Applications to Security (VISSAS 2005), E. Clarke, M. Minea, and F. Tiplea, Eds. IOS Press, 2005, pp. 185–211.
- F. L. Ţiplea, C. Enea, C. V. Bı̂rjoveanu, and I. Boureanu, “Secrecy for bounded protocols with freshness check is NEXPTIME-complete,” Journal of Computer Security, vol. 16, pp. 689– 712, Dec 2008. http://dx.doi.org/10.3233/JCS-2007-0306. [Online]. Available: http://dx.doi.org/10.3233/JCS-2007-0306
- D. Dolev and A. Yao, “On the security of public-key protocols,” IEEE Transactions on Information Theory, vol. 29, no. 2, pp. 198–208, 1983. http://dx.doi.org/10.1109/TIT.1983.1056650. [Online]. Available: http://dx.doi.org/10.1109/TIT.1983.1056650
- R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning About Knowledge. The MIT Press, 2003.
- A. Lomuscio, H. Qu, and F. Raimondi, “MCMAS: A model checker for the verification of multi-agent systems,” in Computer Aided Verification, ser. Lecture Notes in Computer Science, A. Bouajjani and O. Maler, Eds. Springer Berlin Heidelberg, 2009, pp. 682–688. [Online]. Available: http://dx.doi.org/10.1007/978-3-642-02658-4_55
- ——, “MCMAS: An open-source model checker for the verification of multi-agent systems,” International Journal on Software Tools for Technology Transfer, pp. 1–22, 2015. http://dx.doi.org/10.1007/s10009-015-0378-x. [Online]. Available: http://dx.doi.org/10.1007/s10009-015-0378-x
- M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of probabilistic real-time systems,” in Proceedings of the 23rd International Conference on Computer Aided Verification. Springer-Verlag, 2011. http://dx.doi.org/10.1007/978-3-642-22110-1_47 pp. 585–591.