The Design and Analysis of Real-World Cryptographic Protocols

Samuel Scott

The Design and Analysis of Real-World Cryptographic Protocols

Research output: Thesis › Doctoral Thesis

684 Downloads (Pure)

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.

Original language	English
Qualification	Ph.D.
Awarding Institution	Royal Holloway, University of London
Supervisors/Advisors	Paterson, Kenneth, Supervisor Blackburn, Simon, Advisor
Thesis sponsors	Eng & Phys Sci Res Council EPSRC
Award date	1 Feb 2018
Publication status	Unpublished - 2018

Keywords

Cryptography
Protocol analysis
Provable Security

Access to Document

2018scottsphd.pdfOther version, 1.15 MB

4 Conference contribution
1 Paper
1 Article

A Comprehensive Symbolic Analysis of TLS 1.3
Cremers, C., Horvat, M., Hoyland, J., Scott, S. & van der Merwe, T., 30 Oct 2017, ACM SIGSAC Conference on Computer and Commuincations Security. ACM, p. 1773-1788 16 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Key Rotation for Authenticated Encryption
Everspaugh, A., Paterson, K., Ristenpart, T. & Scott, S., 2 Aug 2017, (E-pub ahead of print) Advances in Cryptology – CRYPTO 2017 : 37th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 20–24, 2017, Proceedings, Part III. Springer, p. 98-129 32 p. (Lecture Notes in Computer Science ; vol. 10403 ).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Open Access
File

317 Downloads (Pure)
Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication
Cremers, C., Horvat, M., Scott, S. & Van Der Merwe, T., 18 Aug 2016, IEEE Symposium on Security and Privacy 2016. p. 470-485 16 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Cite this

@phdthesis{d4769ddbb96941c69261f234d4caca9b,

title = "The Design and Analysis of Real-World Cryptographic Protocols",

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.",

keywords = "Cryptography, Protocol analysis, Provable Security",

author = "Samuel Scott",

year = "2018",

language = "English",

school = "Royal Holloway, University of London",

}

TY - BOOK

T1 - The Design and Analysis of Real-World Cryptographic Protocols

AU - Scott, Samuel

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

KW - Cryptography

KW - Protocol analysis

KW - Provable Security

M3 - Doctoral Thesis

ER -

The Design and Analysis of Real-World Cryptographic Protocols

Abstract

Keywords

Access to Document

Research output

A Comprehensive Symbolic Analysis of TLS 1.3

Key Rotation for Authenticated Encryption

Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication

Cite this