Doctoral thesis (Dissertations and theses)
Design and Verification of Specialised Security Goals for Protocol Families
Smith, Zachary Daniel
2020
 

Files


Full Text
zs-thesis-081220.pdf
Publisher postprint (1.99 MB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
Communication Protocols; Automated Verification; Multiset Rewriting
Abstract :
[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.
Disciplines :
Computer science
Author, co-author :
Smith, Zachary Daniel ;  University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Language :
English
Title :
Design and Verification of Specialised Security Goals for Protocol Families
Defense date :
September 2020
Number of pages :
204
Institution :
Unilu - University of Luxembourg, Luxembourg
Degree :
Docteur en Informatique
Promotor :
President :
Jury member :
Cremers, Cas
Kremer, Steve
Trujillo-Rasua, Rolando
Focus Area :
Security, Reliability and Trust
Available on ORBilu :
since 14 December 2020

Statistics


Number of views
153 (18 by Unilu)
Number of downloads
496 (19 by Unilu)

Bibliography


Similar publications



Contact ORBilu