An Intruder Model for Verifying Termination in Security Protocols

J.G. Cederquist; M.T. Dashti

An Intruder Model for Verifying Termination in Security Protocols

J.G. Cederquist, M.T. Dashti

Research output: Book/Report › Report › Professional

110 Downloads (Pure)

Abstract

We formally describe an intruder that is suitable for checking fairness properties of security protocols. The intruder is proved to be equivalent to the Dolev-Yao intruder that respects the resilient communication channels assumption, in the sense that, if a fairness property holds in one of these models, it also holds in the other.

Original language	Undefined
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	13
Publication status	Published - Jul 2005

Publication series

Name	CTIT Technical Report Series
No.	05-29
ISSN (Print)	1381-3625

Keywords

IR-54532
METIS-228788
SCS-Cybersecurity
EWI-723

Access to Document

cederquistFinal published version, 176 KB

Cite this

@book{bef1a4f510b042978c5bbfebcc2c5c61,

title = "An Intruder Model for Verifying Termination in Security Protocols",

abstract = "We formally describe an intruder that is suitable for checking fairness properties of security protocols. The intruder is proved to be equivalent to the Dolev-Yao intruder that respects the resilient communication channels assumption, in the sense that, if a fairness property holds in one of these models, it also holds in the other.",

keywords = "IR-54532, METIS-228788, SCS-Cybersecurity, EWI-723",

author = "J.G. Cederquist and M.T. Dashti",

year = "2005",

month = jul,

language = "Undefined",

series = "CTIT Technical Report Series",

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

number = "05-29",

address = "Netherlands",

}

TY - BOOK

T1 - An Intruder Model for Verifying Termination in Security Protocols

AU - Cederquist, J.G.

AU - Dashti, M.T.

PY - 2005/7

Y1 - 2005/7

N2 - We formally describe an intruder that is suitable for checking fairness properties of security protocols. The intruder is proved to be equivalent to the Dolev-Yao intruder that respects the resilient communication channels assumption, in the sense that, if a fairness property holds in one of these models, it also holds in the other.

AB - We formally describe an intruder that is suitable for checking fairness properties of security protocols. The intruder is proved to be equivalent to the Dolev-Yao intruder that respects the resilient communication channels assumption, in the sense that, if a fairness property holds in one of these models, it also holds in the other.

KW - IR-54532

KW - METIS-228788

KW - SCS-Cybersecurity

KW - EWI-723

M3 - Report

T3 - CTIT Technical Report Series

BT - An Intruder Model for Verifying Termination in Security Protocols

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -