Timed Model Checking of Security Protocols

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

Timed Model Checking of Security Protocols

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

Research output: Book/Report › Report › Other research output

32 Citations (Scopus)

104 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
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	355
Publication status	Published - Jun 2004

Publication series

Name	CTIT technical report series
Publisher	University of Twente, Centre for Telematics and Information Technology (CTIT)
No.	TR-CTIT-04-24

Keywords

EWI-6047
SCS-Cybersecurity
IR-56999

Access to Document

http://www.ub.utwente.nl/webdocs/ctit/1/000000fb.pdf

Cite this

@book{4b746fc4f0684274a7579d4898c75607,

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-6047, SCS-Cybersecurity, IR-56999",

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

year = "2004",

month = jun,

language = "Undefined",

series = "CTIT technical report series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "TR-CTIT-04-24",

address = "Netherlands",

}

TY - BOOK

T1 - Timed Model Checking of Security Protocols

AU - Corin, R.J.

AU - Etalle, Sandro

AU - Hartel, Pieter H.

AU - Mader, Angelika H.

PY - 2004/6

Y1 - 2004/6

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-6047

KW - SCS-Cybersecurity

KW - IR-56999

M3 - Report

T3 - CTIT technical report series

BT - Timed Model Checking of Security Protocols

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -