Operational semantics of security protocols

C.J.F. Cremers; S. Mauw

doi:10.1007/11495628_4

Operational semantics of security protocols

C.J.F. Cremers, S. Mauw

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

38 Citations (Scopus)

Abstract

Based on a concise domain analysis we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analysing the Needham-Schroeder-Lowe protocol.

Original language	English
Title of host publication	Scenarios : Models, Transformations and Tools
Subtitle of host publication	International Workshop, Dagstuhl Castle, Germany, September 7-12, 2003, Revised selected papers
Editors	S. Leue, T.J. Systä
Place of Publication	Berlin
Publisher	Springer
Chapter	4
Pages	66-89
Number of pages	24
ISBN (Electronic)	978-3-540-32032-6
ISBN (Print)	3-540-26189-3, 978-3-540-26189-6
DOIs	https://doi.org/10.1007/11495628_4
Publication status	Published - 2005

Publication series

Name	Lecture Notes in Computer Science (LNCS)
Volume	3466
ISSN (Print)	0302-9743

Access to Document

10.1007/11495628_4

Cite this

Cremers, C. J. F., & Mauw, S. (2005). Operational semantics of security protocols. In S. Leue, & T. J. Systä (Eds.), Scenarios : Models, Transformations and Tools : International Workshop, Dagstuhl Castle, Germany, September 7-12, 2003, Revised selected papers (pp. 66-89). (Lecture Notes in Computer Science (LNCS); Vol. 3466). Springer. https://doi.org/10.1007/11495628_4

@inproceedings{5fb9de915e0f49dc80f7ad63917e1481,

title = "Operational semantics of security protocols",

abstract = "Based on a concise domain analysis we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analysing the Needham-Schroeder-Lowe protocol.",

author = "C.J.F. Cremers and S. Mauw",

year = "2005",

doi = "10.1007/11495628_4",

language = "English",

isbn = "3-540-26189-3",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "66--89",

editor = "S. Leue and T.J. Syst{\"a}",

booktitle = "Scenarios : Models, Transformations and Tools",

address = "Germany",

}

Operational semantics of security protocols. / Cremers, C.J.F.; Mauw, S.
Scenarios : Models, Transformations and Tools : International Workshop, Dagstuhl Castle, Germany, September 7-12, 2003, Revised selected papers. ed. / S. Leue; T.J. Systä. Berlin: Springer, 2005. p. 66-89 (Lecture Notes in Computer Science (LNCS); Vol. 3466).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Operational semantics of security protocols

AU - Cremers, C.J.F.

AU - Mauw, S.

PY - 2005

Y1 - 2005

N2 - Based on a concise domain analysis we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analysing the Needham-Schroeder-Lowe protocol.

AB - Based on a concise domain analysis we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analysing the Needham-Schroeder-Lowe protocol.

U2 - 10.1007/11495628_4

DO - 10.1007/11495628_4

M3 - Conference contribution

SN - 3-540-26189-3

SN - 978-3-540-26189-6

T3 - Lecture Notes in Computer Science (LNCS)

SP - 66

EP - 89

BT - Scenarios : Models, Transformations and Tools

A2 - Leue, S.

A2 - Systä, T.J.

PB - Springer

CY - Berlin

ER -

Operational semantics of security protocols

Abstract

Publication series

Access to Document

Fingerprint

Cite this