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

Cite this

Hess, A. V., & Modersheim, S. (2018). A Typing Result for Stateful Protocols. In 2018 IEEE 31st Computer Security Foundations Symposium (Vol. 2018-July, pp. 374-388). IEEE. I E E E Computer Security Foundations Symposium. Proceedings https://doi.org/10.1109/CSF.2018.00034
Hess, Andreas Viktor ; Modersheim, Sebastian. / A Typing Result for Stateful Protocols. 2018 IEEE 31st Computer Security Foundations Symposium. Vol. 2018-July IEEE, 2018. pp. 374-388 (I E E E Computer Security Foundations Symposium. Proceedings).
@inproceedings{879ccdbc74cc4267aac9c28212c86b7c,
title = "A Typing Result for Stateful Protocols",
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.",
author = "Hess, {Andreas Viktor} and Sebastian Modersheim",
year = "2018",
doi = "10.1109/CSF.2018.00034",
language = "English",
volume = "2018-July",
pages = "374--388",
booktitle = "2018 IEEE 31st Computer Security Foundations Symposium",
publisher = "IEEE",
address = "United States",

}

Hess, AV & Modersheim, S 2018, A Typing Result for Stateful Protocols. in 2018 IEEE 31st Computer Security Foundations Symposium. vol. 2018-July, IEEE, I E E E Computer Security Foundations Symposium. Proceedings, pp. 374-388. https://doi.org/10.1109/CSF.2018.00034

A Typing Result for Stateful Protocols. / Hess, Andreas Viktor; Modersheim, Sebastian.

2018 IEEE 31st Computer Security Foundations Symposium. Vol. 2018-July IEEE, 2018. p. 374-388 (I E E E Computer Security Foundations Symposium. Proceedings).

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

TY - GEN

T1 - A Typing Result for Stateful Protocols

AU - Hess, Andreas Viktor

AU - Modersheim, Sebastian

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

U2 - 10.1109/CSF.2018.00034

DO - 10.1109/CSF.2018.00034

M3 - Article in proceedings

VL - 2018-July

SP - 374

EP - 388

BT - 2018 IEEE 31st Computer Security Foundations Symposium

PB - IEEE

ER -

Hess AV, Modersheim S. A Typing Result for Stateful Protocols. In 2018 IEEE 31st Computer Security Foundations Symposium. Vol. 2018-July. IEEE. 2018. p. 374-388. (I E E E Computer Security Foundations Symposium. Proceedings). https://doi.org/10.1109/CSF.2018.00034