Bounding Messages for Free in Security Protocols

Myrto Arapinis, Marie Duflot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


The verification of security protocols has been proven to be undecidable in general. Different 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, therefore bounding message length. In this paper, we show how to get message boundedness “for free” under a reasonable (syntactic) assumption on protocols, which we call well-formedness. This enables us to improve existing decidability results.
Original languageEnglish
Title of host publicationFSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science
Subtitle of host publication27th International Conference, New Delhi, India, December 12-14, 2007. Proceedings
EditorsV. Arvind, Sanjiva Prasad
PublisherSpringer Berlin Heidelberg
Number of pages12
ISBN (Electronic)978-3-540-77050-3
ISBN (Print)978-3-540-77049-7
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'Bounding Messages for Free in Security Protocols'. Together they form a unique fingerprint.

Cite this