Abstract
Designing cryptographic protocols for use in the real world is a challenging
task, requiring a fine balance between practicality and security. Ad hoc
constructions are often catastrophically broken, and even well-studied
protocols regularly do not stand up to the test of time. We look at some of
the ways cryptographic protocols are designed and analysed, applying these
techniques to a variety of real-word scenarios.
Our first scenario considers password storage, introducing
a new primitive called a verifiable, partially oblivious PRF. We analyse the
suitability of this primitive to the application in question, provide
formal security proofs, and evaluate an example instantiation.
The second scenario introduces a new security model to better understand the
domain of key rotation for authenticated encryption. This is an area highly
relevant to modern practices of storing data encrypted in the cloud. By
introducing this new security model, we show that existing solutions fall
short of achieving any meaningful security properties, and suggest some
simple fixes. Finally, we implement and prove a new construction which meets
our strongest definition, and analyse its practicality.
Finally, to contrast with the computational approach in previous chapters,
we additionally consider symbolic approaches to security analysis, using the
formal verification tool Tamarin to prove security properties of the latest
draft of the TLS 1.3 specification. Our results show formal method
complement other approaches nicely, and provide a new perspective.
task, requiring a fine balance between practicality and security. Ad hoc
constructions are often catastrophically broken, and even well-studied
protocols regularly do not stand up to the test of time. We look at some of
the ways cryptographic protocols are designed and analysed, applying these
techniques to a variety of real-word scenarios.
Our first scenario considers password storage, introducing
a new primitive called a verifiable, partially oblivious PRF. We analyse the
suitability of this primitive to the application in question, provide
formal security proofs, and evaluate an example instantiation.
The second scenario introduces a new security model to better understand the
domain of key rotation for authenticated encryption. This is an area highly
relevant to modern practices of storing data encrypted in the cloud. By
introducing this new security model, we show that existing solutions fall
short of achieving any meaningful security properties, and suggest some
simple fixes. Finally, we implement and prove a new construction which meets
our strongest definition, and analyse its practicality.
Finally, to contrast with the computational approach in previous chapters,
we additionally consider symbolic approaches to security analysis, using the
formal verification tool Tamarin to prove security properties of the latest
draft of the TLS 1.3 specification. Our results show formal method
complement other approaches nicely, and provide a new perspective.
Original language | English |
---|---|
Qualification | Ph.D. |
Awarding Institution |
|
Supervisors/Advisors |
|
Thesis sponsors | |
Award date | 1 Feb 2018 |
Publication status | Unpublished - 2018 |
Keywords
- Cryptography
- Protocol analysis
- Provable Security