Epistemic verification of anonymity

J. Eijck, van, S.M. Orzan

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

29 Citations (Scopus)
1 Downloads (Pure)


Anonymity is not a trace-based property, therefore traditional model checkers are not directly able to express it and verify it. However, by using epistemic logic (logic of knowledge) to model the protocols, anonymity becomes an easily verifiable epistemic formula. We propose using Dynamic Epistemic Logic to model security protocols and properties, in particular anonymity properties. We have built tool support for DEL verification which reuses state-of-the-art tool support for automata-based verification. We illustrate this approach by analyzing an anonymous broadcast protocol and an electronic voting protocol. By comparison with a process-based analysis of the same protocols, we also discuss the relative (dis)advantages of the process-based and epistemic-based verification methods in general.
Original languageEnglish
Title of host publicationProceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy
EditorsF. Gadducci
Publication statusPublished - 2007
Eventconference; VODCA 2006, Bertinoro, Italy; 2007-09-16; 2007-09-17 -
Duration: 16 Sept 200717 Sept 2007

Publication series

NameElectronic Notes in Theoretical Computer Science
ISSN (Print)1571-0061


Conferenceconference; VODCA 2006, Bertinoro, Italy; 2007-09-16; 2007-09-17
OtherVODCA 2006, Bertinoro, Italy


Dive into the research topics of 'Epistemic verification of anonymity'. Together they form a unique fingerprint.

Cite this