Abstract
We present a powerful and flexible method for automatically checking anonymity in a possibilistic general-purpose process algebraic verification toolset. We propose new definitions of a choice anonymity degree and a player anonymity degree, to quantify the precision with which an intruder is able to single out the true originator of a given event or to associate the right event to a given protocol participant. We show how these measures of anonymity can be automatically calculated from a protocol specification in μCRL, by using a combination of dedicated tools and existing state-of-the-art μCRL tools. To illustrate the flexibility of our method we test the Dining Cryptographers problem and the FOO 92 voting protocol. Our definitions of anonymity provide an accurate picture of the different ways that anonymity can break down, due for instance to coallitions of inside intruders. Our calculations can be performed on a cluster of machines, allowing us to check protocols for large numbers of participants.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), 77–121 (1985)
Berthold, O., Pfiztmann, A., Standtke, R.: The disavantages of free mix routes and how to overcome them. In: Federrath, H. (ed.) Proc. Workshop on Design Issues in Anonymity and Unobservability. LNCS, vol. 2009, pp. 30–45. Springer, Heidelberg (2001)
Bhargava, M., Palamidessi, C.: Probabilistic anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)
Blom, S.C.C., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.C.: μCRL: A toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)
Blom, S.C.C., Groote, J.F., Mauw, S., Serebrenik, A.: Analysing the BKE-security protocol with μCRL. In: Proc. 6th AMAST Workshop on Real-Time Systems. ENTCS, vol. 139, pp. 49–90 (2004)
Blom, S.C.C., Orzan, S.M.: A distributed algorithm for strong bisimulation reduction of state spaces. Software Tools for Technology Transfer 7(1), 74–86 (2005)
Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1, 65–75 (1988)
Chothia, T.: Analysing the mute anonymous file-sharing system using the pi-calculus. In: Najm, E., Pradat-Peyre, J.F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 115–130. Springer, Heidelberg (2006)
Chothia, T., Orzan, S.M., Pang, J.: μCRL specifications. http://www.win.tue.nl/~sorzan/anonymity
Deng, Y., Palamidessi, C., Pang, J.: Weak probabilistic anonymity. In: Proc. 3rd Workshop on Security Issues in Concurrency (2005)
Díaz, C., Seys, S., Claessens, J., Preneel, B.: Towards measuring anonymity. In: PET 2002. LNCS, vol. 2482, pp. 54–68. Springer, Heidelberg (2002)
van Eijck, J., Orzan, S.M.: Epistemic verification of anonymity. In: Proc. Views On Designing Complex Architectures (VODCA 2006) (2006)
Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1992)
Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Proc. 3rd ACM Workshop on Formal Methods in Security Engineering, pp. 63–72. ACM Press, New York (2005)
Groote, J.F., Reniers, M.A.: Algebraic process verification. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, North-Holland, pp. 1151–1208 (2001)
Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. Journal of Computer Security, 483–514 (2005)
Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: A modular approach. Journal of Computer Security 12(1), 3–36 (2004)
Hüttel, H., Shukla, S.: On the complexity of deciding behavioural equivalences and preorders - a survey. Technical Report RS-96-39, BRICS (1996)
Kremer, S., Ryan, M.: Analysis of an electronic voting protocol in the applied pi-calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)
Lomuscio, A., Raimondi, F.: MCMAS: A tool for verifying multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)
Mauw, S., Verschuren, J., de Vink, E.P.: A formalization of anonymity and onion routing. In: Samarati, P., Ryan, P.Y A, Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 109–124. Springer, Heidelberg (2004)
Mauw, S., Verschuren, J., de Vink, E.P.: Data anonymity in the FOO voting scheme. In: Proc. Views On Designing Complex Architectures (VODCA 2006) (2006)
Meritt, M.J.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (1983)
van der Meyden, R., Su, K.: Symbolic model checking the knowledge of the dining cryptographers. In: Proc. 17th IEEE Computer Security Foundations Workshop, pp. 280–291. IEEE Computer Society Press, Los Alamitos (2004)
Pang, J.: Analysis of a security protocol in μCRL. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 396–400. Springer, Heidelberg (2002)
Pfitzmann, A., Hansen, M.: Anonymity, unobservability, and pseudonymity: A proposal for terminology, draft v0.23 (August 2005)
Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for Web transactions. ACM Transactions on Information and System Security 1(1), 66–92 (1998)
Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) Computer Security - ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)
Serjantov, A., Danezis, G.: Towards an information theoretic metric for anonymity. In: Dingledine, R., Syverson, P.F. (eds.) PET 2002. LNCS, vol. 2482, pp. 41–53. Springer, Heidelberg (2003)
Shmatikov, V.: Probabilistic model checking of an anonymity system. Journal of Computer Security 12(3/4), 355–377 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chothia, T., Orzan, S., Pang, J., Torabi Dashti, M. (2007). A Framework for Automatically Checking Anonymity with μCRL. In: Montanari, U., Sannella, D., Bruni, R. (eds) Trustworthy Global Computing. TGC 2006. Lecture Notes in Computer Science, vol 4661. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75336-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-75336-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75333-9
Online ISBN: 978-3-540-75336-0
eBook Packages: Computer ScienceComputer Science (R0)