Epistemic verification of anonymity

J. Eijck, van, S.M. Orzan

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

28 Citations (Scopus)
1 Downloads (Pure)

Abstract

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
Pages159-174
DOIs
Publication statusPublished - 2007
Eventconference; VODCA 2006, Bertinoro, Italy; 2007-09-16; 2007-09-17 -
Duration: 16 Sep 200717 Sep 2007

Publication series

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

Conference

Conferenceconference; VODCA 2006, Bertinoro, Italy; 2007-09-16; 2007-09-17
Period16/09/0717/09/07
OtherVODCA 2006, Bertinoro, Italy

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

Cite this