A framework for automatically checking anonymity with μ CRL

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

22 Citaten (Scopus)
153 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.
Originele taal-2Engels
TitelRevised Selected Papers of the Second Symposium on Trustworthy Global Computing (TGC 2006) 7-9 November 2006, Lucca, Italy
RedacteurenU. Montanari, D. Sannella, R. Bruni
Plaats van productieBerlin, Germany
ISBN van geprinte versie978-3-540-75333-9
StatusGepubliceerd - 2007
Evenementconference; TGC 2006, Lucca, Italy; 2006-11-07; 2006-11-09 -
Duur: 7 nov. 20069 nov. 2006

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


Congresconference; TGC 2006, Lucca, Italy; 2006-11-07; 2006-11-09
AnderTGC 2006, Lucca, Italy


Duik in de onderzoeksthema's van 'A framework for automatically checking anonymity with μ CRL'. Samen vormen ze een unieke vingerafdruk.

Citeer dit