A Typing Result for Stateful Protocols - Extended Version

Andreas Viktor Hess, Sebastian Alexander Mödersheim

Research output: Book/ReportReportResearchpeer-review

127 Downloads (Pure)


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-π, AIF-ω, 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
PublisherDTU Compute
Number of pages48
Publication statusPublished - 2018
SeriesDTU Compute Technical Report-2018


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

Cite this