| 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 | |||
| http://hdl.handle.net/10993/45058 | |||
| Design and Verification of Specialised Security Goals for Protocol Families | |
| English | |
Smith, Zachary Daniel  [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >] | |
| Sep-2020 | |
| University of Luxembourg, Luxembourg | |
| Docteur en Informatique | |
| 204 | |
| Mauw, Sjouke | |
| Ryan, Peter Y A | |
| 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. | |
| http://hdl.handle.net/10993/45058 |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
