A Typing Result for Stateful Protocols

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

There are several typing results that, for certain classes of protocols, show it is without loss of attacks to restrict the intruder to sending only well-typed messages. So far, all these typing results hold only for relatively simple protocols that do not keep a state beyond single sessions, excluding stateful protocols that, e.g., maintain long-term databases. Recently, several verification tools for stateful protocols have been proposed, e.g., Set-pi, AIF-omega, and SAPIC/Tamarin, but for none of these a typing result has been established. The main contribution of this paper is a typing result, for a large class of stateful protocols, based on a symbolic protocol model. We illustrate how to connect several formalisms for stateful protocols to this symbolic model. Finally, we discuss how the conditions of our typing result apply to existing protocols, or can be achieved by minor modifications.
Original languageEnglish
Title of host publication2018 IEEE 31st Computer Security Foundations Symposium
Number of pages15
Volume2018-July
PublisherIEEE
Publication date2018
Pages374-388
DOIs
Publication statusPublished - 2018
SeriesI E E E Computer Security Foundations Symposium. Proceedings
ISSN1940-1434

Fingerprint Dive into the research topics of 'A Typing Result for Stateful Protocols'. Together they form a unique fingerprint.

Cite this