Timed Model Checking of Security Protocols

R.J. Corin; Sandro Etalle; Pieter H. Hartel; Angelika H. Mader

doi:10.1145/1029133.1029137

Timed Model Checking of Security Protocols

R.J. Corin, Sandro Etalle, Pieter H. Hartel, Angelika H. Mader

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

249 Downloads (Pure)

Abstract

We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows the study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time.

Original language	Undefined
Title of host publication	2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)
Editors	V. Atluri, M. Backes, D.A. Basin, M. Waidner
Place of Publication	New York
Publisher	ACM Press
Pages	23-32
Number of pages	10
ISBN (Print)	1-58113-971-3
DOIs	https://doi.org/10.1145/1029133.1029137
Publication status	Published - Oct 2004
Event	2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE) - Fairfax, Virginia Duration: 1 Oct 2004 → 1 Oct 2004

Publication series

Name
Publisher	ACM Press

Workshop

Workshop	2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)
Period	1/10/04 → 1/10/04

Keywords

EWI-766
IR-48643
METIS-220303
SCS-Cybersecurity

Access to Document

10.1145/1029133.1029137

http://doi.acm.org/10.1145/1029133.1029137

Cite this

@inproceedings{e7cfd444993b4393b68c03c8b1018a38,

title = "Timed Model Checking of Security Protocols",

abstract = "We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows the study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time.",

keywords = "EWI-766, IR-48643, METIS-220303, SCS-Cybersecurity",

author = "R.J. Corin and Sandro Etalle and Hartel, {Pieter H.} and Mader, {Angelika H.}",

note = "Imported from DIES; 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE) ; Conference date: 01-10-2004 Through 01-10-2004",

year = "2004",

month = oct,

doi = "10.1145/1029133.1029137",

language = "Undefined",

isbn = "1-58113-971-3",

publisher = "ACM Press",

pages = "23--32",

editor = "V. Atluri and M. Backes and D.A. Basin and M. Waidner",

booktitle = "2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)",

}

Corin, RJ, Etalle, S, Hartel, PH & Mader, AH 2004, Timed Model Checking of Security Protocols. in V Atluri, M Backes, DA Basin & M Waidner (eds), 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE). ACM Press, New York, pp. 23-32, 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE), 1/10/04. https://doi.org/10.1145/1029133.1029137

Timed Model Checking of Security Protocols. / Corin, R.J.; Etalle, Sandro; Hartel, Pieter H. et al.
2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE). ed. / V. Atluri; M. Backes; D.A. Basin; M. Waidner. New York: ACM Press, 2004. p. 23-32.

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

TY - GEN

T1 - Timed Model Checking of Security Protocols

AU - Corin, R.J.

AU - Etalle, Sandro

AU - Hartel, Pieter H.

AU - Mader, Angelika H.

N1 - Imported from DIES

PY - 2004/10

Y1 - 2004/10

N2 - We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows the study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time.

AB - We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows the study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time.

KW - EWI-766

KW - IR-48643

KW - METIS-220303

KW - SCS-Cybersecurity

U2 - 10.1145/1029133.1029137

DO - 10.1145/1029133.1029137

M3 - Conference contribution

SN - 1-58113-971-3

SP - 23

EP - 32

BT - 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)

A2 - Atluri, V.

A2 - Backes, M.

A2 - Basin, D.A.

A2 - Waidner, M.

PB - ACM Press

CY - New York

T2 - 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE)

Y2 - 1 October 2004 through 1 October 2004

ER -