Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

Pieter Ceelen; Sjouke Mauw; Saša Radomirović

doi:10.1016/j.entcs.2007.12.015

Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

Pieter Ceelen^*, Sjouke Mauw, Saša Radomirović

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

4 Citations (Scopus)

52 Downloads (Pure)

Abstract

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability. Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.

Original language	English
Pages (from-to)	31-43
Number of pages	13
Journal	Electronic Notes in Theoretical Computer Science
Volume	197
Issue number	2
DOIs	https://doi.org/10.1016/j.entcs.2007.12.015
Publication status	Published - 22 Feb 2008

Keywords

automatic verification
security protocols
semantics
type-flaw attacks

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/j.entcs.2007.12.015Licence: CC BY-NC-ND

Download pdfFinal published version, 312 KBLicence: CC BY-NC-ND

Cite this

@article{e64a6d7b77e94ee48fbd185b18d22a2e,

title = "Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks",

abstract = "In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability. Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.",

keywords = "automatic verification, security protocols, semantics, type-flaw attacks",

author = "Pieter Ceelen and Sjouke Mauw and Sa{\v s}a Radomirovi{\'c}",

year = "2008",

month = feb,

day = "22",

doi = "10.1016/j.entcs.2007.12.015",

language = "English",

volume = "197",

pages = "31--43",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "2",

}

TY - JOUR

T1 - Chosen-name Attacks

T2 - An Overlooked Class of Type-flaw Attacks

AU - Ceelen, Pieter

AU - Mauw, Sjouke

AU - Radomirović, Saša

PY - 2008/2/22

Y1 - 2008/2/22

N2 - In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability. Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.

AB - In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability. Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.

KW - automatic verification

KW - security protocols

KW - semantics

KW - type-flaw attacks

UR - http://www.scopus.com/inward/record.url?scp=39149126358&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.12.015

DO - 10.1016/j.entcs.2007.12.015

M3 - Article

AN - SCOPUS:39149126358

SN - 1571-0661

VL - 197

SP - 31

EP - 43

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

ER -

Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this