Reference : Design and Verification of Specialised Security Goals for Protocol Families
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Design and Verification of Specialised Security Goals for Protocol Families
Smith, Zachary Daniel mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
University of Luxembourg, ​​Luxembourg
Docteur en Informatique
Mauw, Sjouke mailto
Ryan, Peter Y A mailto
Cremers, Cas
Kremer, Steve
Trujillo-Rasua, Rolando
[en] Communication Protocols ; Automated Verification ; Multiset Rewriting
[en] Communication Protocols form a fundamental backbone of our modern information networks. These protocols provide a framework to describe how agents - Computers, Smartphones, RFID Tags and more - should structure their communication. As a result, the security of these protocols is implicitly trusted to protect our personal data. In 1997, Lowe presented ‘A Hierarchy of Authentication Specifications’, formalising a set of security requirements that might be expected of communication protocols. The value of these requirements is that they can be formally tested and verified against a protocol specification. This allows a user to have confidence that their communications are protected in ways that are uniformly defined and universally agreed upon.

Since that time, the range of objectives and applications of real-world protocols has grown. Novel requirements - such as checking the physical distance between participants, or evolving trust assumptions of intermediate nodes on the network - mean that new attack vectors are found on a frequent basis. The challenge, then, is to define security goals which will guarantee security, even when the nature of these attacks is not known.

In this thesis, a methodology for the design of security goals is created. It is used to define a collection of specialised security goals for protocols in multiple different families, by considering tailor-made models for these specific scenarios. For complex requirements, theorems are proved that simplify analysis, allowing the verification of security goals to be efficiently modelled in automated prover tools.

File(s) associated to this reference

Fulltext file(s):

Open access
zs-thesis-081220.pdfPublisher postprint1.94 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.