Data access specification and the most powerful symbolic attacker in MSR

10Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Most systems designed for the symbolic verification of security protocols operate under the unproved assumption that an attack can only result from the combination of a fixed number of message transformations, which altogether constitute the capabilities of the so-called Dolev-Yao intruder. In this paper, we show that the Dolev-Yao intruder can indeed emulate the actions of an arbitrary symbolic adversary. In order to do so, we extend MSR, a flexible specification framework for security protocols based on typed multiset rewriting, with a static check called data access specification and aimed at catching specification errors such as a principal trying to use a key that she is not entitled to access. © Springer-Verlag Berlin Heidelberg 2003.

Cite

CITATION STYLE

APA

Cervesato, I. (2003). Data access specification and the most powerful symbolic attacker in MSR. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2609, 384–416. https://doi.org/10.1007/3-540-36532-x_23

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free