Bounding messages for free in security protocols - extension to various security properties

Myrto Arapinis, Marie Duflot

Research output: Contribution to journalArticlepeer-review

Abstract

While the verification of security protocols has been proved to be undecidable in general, several approaches use simplifying hypotheses in order to obtain decidability for interesting subclasses. Amongst the most common is type abstraction, i.e. considering only well-typed runs of the protocol, therefore bounding message length. In this paper, we show how to get message boundedness “for free” under a reasonable (syntactic) assumption on protocols, in order to verify a variety of interesting security properties including secrecy and several authentication properties. This enables us to improve existing decidability results by restricting the search space for attacks.
Original languageEnglish
Pages (from-to)182-215
Number of pages34
JournalInformation and Computation
Volume239
DOIs
Publication statusPublished - 2014

Fingerprint

Dive into the research topics of 'Bounding messages for free in security protocols - extension to various security properties'. Together they form a unique fingerprint.

Cite this