Static Validation of Security Protocols

Chiara Bodei; Mikael Buchholtz; P. Degano; Hanne Riis Nielson; Flemming Nielson

Static Validation of Security Protocols

Chiara Bodei, Mikael Buchholtz, P. Degano, Hanne Riis Nielson, Flemming Nielson

Research output: Contribution to journal › Journal article › Research › peer-review

Abstract

We methodically expand protocol narrations into terms of a process algebra in order to specify some of the 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 to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham-Schroeder symmetric key, Otway-Rees, Yahalom, Andrew secure RPC, Needham-Schroeder asymmetric key, and Beller-Chang-Yacobi MSR

Original language	English
Journal	Journal of Computer Security
Volume	13
Issue number	3
Pages (from-to)	347-390
ISSN	0926-227X
Publication status	Published - 2005

Bibliographical note

11 charts

Cite this

Bodei, C., Buchholtz, M., Degano, P., Nielson, H. R., & Nielson, F. (2005). Static Validation of Security Protocols. Journal of Computer Security, 13(3), 347-390.

@article{1a12a563e23942e1847a6af0323a3ec2,

title = "Static Validation of Security Protocols",

abstract = "We methodically expand protocol narrations into terms of a process algebra in order to specify some of the 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 to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham-Schroeder symmetric key, Otway-Rees, Yahalom, Andrew secure RPC, Needham-Schroeder asymmetric key, and Beller-Chang-Yacobi MSR",

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

note = "11 charts",

year = "2005",

language = "English",

volume = "13",

pages = "347--390",

journal = "Journal of Computer Security",

issn = "0926-227X",

publisher = "I O S Press",

number = "3",

}

TY - JOUR

T1 - Static Validation of Security Protocols

AU - Bodei, Chiara

AU - Buchholtz, Mikael

AU - Degano, P.

AU - Nielson, Hanne Riis

AU - Nielson, Flemming

N1 - 11 charts

PY - 2005

Y1 - 2005

N2 - We methodically expand protocol narrations into terms of a process algebra in order to specify some of the 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 to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham-Schroeder symmetric key, Otway-Rees, Yahalom, Andrew secure RPC, Needham-Schroeder asymmetric key, and Beller-Chang-Yacobi MSR

AB - We methodically expand protocol narrations into terms of a process algebra in order to specify some of the 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 to identify several authentication flaws in symmetric and asymmetric key protocols such as Needham-Schroeder symmetric key, Otway-Rees, Yahalom, Andrew secure RPC, Needham-Schroeder asymmetric key, and Beller-Chang-Yacobi MSR

M3 - Journal article

VL - 13

SP - 347

EP - 390

JO - Journal of Computer Security

JF - Journal of Computer Security

SN - 0926-227X

IS - 3

ER -