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

Pieter Ceelen, Sjouke Mauw, Saša Radomirović

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
162 Downloads (Pure)


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 languageEnglish
Pages (from-to)31-43
Number of pages13
JournalElectronic Notes in Theoretical Computer Science
Issue number2
Early online date20 Feb 2008
Publication statusPublished - 22 Feb 2008
Event3rd International Workshop on Security and Trust Management - Dresden, Germany
Duration: 27 Sept 200727 Sept 2007


  • Automatic verification
  • Security protocols
  • Semantics
  • Type-flaw attacks

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks'. Together they form a unique fingerprint.

Cite this