A framework for automatically checking anonymity with μ CRL

T. Chothia, S.M. Orzan, J. Pang, M. Torabi Dashti

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

22 Citations (Scopus)
168 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationRevised Selected Papers of the Second Symposium on Trustworthy Global Computing (TGC 2006) 7-9 November 2006, Lucca, Italy
EditorsU. Montanari, D. Sannella, R. Bruni
Place of PublicationBerlin, Germany
ISBN (Print)978-3-540-75333-9
Publication statusPublished - 2007
Eventconference; TGC 2006, Lucca, Italy; 2006-11-07; 2006-11-09 -
Duration: 7 Nov 20069 Nov 2006

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conferenceconference; TGC 2006, Lucca, Italy; 2006-11-07; 2006-11-09
OtherTGC 2006, Lucca, Italy


Dive into the research topics of 'A framework for automatically checking anonymity with μ CRL'. Together they form a unique fingerprint.

Cite this