Epistemic verification of anonymity

J. Eijck, van, S.M. Orzan

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

26 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

Network protocols

Cite this

Eijck, van, J., & Orzan, S. M. (2007). Epistemic verification of anonymity. In F. Gadducci (Ed.), Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy (pp. 159-174). (Electronic Notes in Theoretical Computer Science; Vol. 168). https://doi.org/10.1016/j.entcs.2006.08.026
Eijck, van, J. ; Orzan, S.M. / Epistemic verification of anonymity. Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy. editor / F. Gadducci. 2007. pp. 159-174 (Electronic Notes in Theoretical Computer Science).
@inproceedings{d0936db239ae4cc5bf917b6f8f6e9885,
title = "Epistemic verification of anonymity",
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.",
author = "{Eijck, van}, J. and S.M. Orzan",
year = "2007",
doi = "10.1016/j.entcs.2006.08.026",
language = "English",
series = "Electronic Notes in Theoretical Computer Science",
pages = "159--174",
editor = "F. Gadducci",
booktitle = "Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy",

}

Eijck, van, J & Orzan, SM 2007, Epistemic verification of anonymity. in F Gadducci (ed.), Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy. Electronic Notes in Theoretical Computer Science, vol. 168, pp. 159-174, conference; VODCA 2006, Bertinoro, Italy; 2007-09-16; 2007-09-17, 16/09/07. https://doi.org/10.1016/j.entcs.2006.08.026

Epistemic verification of anonymity. / Eijck, van, J.; Orzan, S.M.

Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy. ed. / F. Gadducci. 2007. p. 159-174 (Electronic Notes in Theoretical Computer Science; Vol. 168).

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

TY - GEN

T1 - Epistemic verification of anonymity

AU - Eijck, van, J.

AU - Orzan, S.M.

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1016/j.entcs.2006.08.026

DO - 10.1016/j.entcs.2006.08.026

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 159

EP - 174

BT - Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy

A2 - Gadducci, F.

ER -

Eijck, van J, Orzan SM. Epistemic verification of anonymity. In Gadducci F, editor, Proceedings Second International Workshop on Views on Designing Complex Architectures (VODCA 2006) 16-17 September 2006, Bertinoro, Italy. 2007. p. 159-174. (Electronic Notes in Theoretical Computer Science). https://doi.org/10.1016/j.entcs.2006.08.026