Automatic Validation of Protocol Narration

Chiara Bodei; Mikael Buchholtz; Pierpablo Degano; Flemming Nielson; Hanne Riis Nielson

Automatic Validation of Protocol Narration

Chiara Bodei, Mikael Buchholtz, Pierpablo Degano, Flemming Nielson, Hanne Riis Nielson

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

We perform a systematic expansion of protocol narrations into terms of a process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.

Original language	English
Title of host publication	Proceedings of the 16th Computer Security Foundations Workshop (CSFW 03).
Publisher	IEEE Computer Society Press
Publication date	2003
Pages	126-140
Publication status	Published - 2003

Access to Document

http://www.imm.dtu.dk/pubdb/p.php?2111

OpenUrl availability

Full text

Cite this

@inproceedings{fd1c40be93bc40a494a4966dc8dbd655,

title = "Automatic Validation of Protocol Narration",

abstract = "We perform a systematic expansion of protocol narrations into terms of a process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.",

author = "Chiara Bodei and Mikael Buchholtz and Pierpablo Degano and Flemming Nielson and Nielson, {Hanne Riis}",

year = "2003",

language = "English",

pages = "126--140",

booktitle = "Proceedings of the 16th Computer Security Foundations Workshop (CSFW 03).",

publisher = "IEEE Computer Society Press",

}

TY - GEN

T1 - Automatic Validation of Protocol Narration

AU - Bodei, Chiara

AU - Buchholtz, Mikael

AU - Degano, Pierpablo

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

PY - 2003

Y1 - 2003

N2 - We perform a systematic expansion of protocol narrations into terms of a process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.

AB - We perform a systematic expansion of protocol narrations into terms of a process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.

M3 - Article in proceedings

SP - 126

EP - 140

BT - Proceedings of the 16th Computer Security Foundations Workshop (CSFW 03).

PB - IEEE Computer Society Press

ER -

Automatic Validation of Protocol Narration

Abstract

Access to Document

OpenUrl availability

Fingerprint

Cite this