A Typing Result for Stateful Protocols - Extended Version

Research output: Book/ReportReportResearchpeer-review

61 Downloads (Pure)

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-π, 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
Volume4

Cite this

Hess, A. V., & Mödersheim, S. A. (2018). A Typing Result for Stateful Protocols - Extended Version. DTU Compute. DTU Compute Technical Report-2018, Vol.. 4