| Summary: | <p>Analysing the security of cryptographic protocols by hand is a challenging endeavour. It requires substantial expertise, weeks of intensive effort and the resulting proof of security often arrives long after the protocol design has been finalised and even deployed. However, automated protocol verification tools, such as Tamarin and ProVerif, offer a compelling alternative as they require less expertise, promise quicker results and have been used to successfully analyse complex real world protocols such as TLS, 5G and Signal.</p>
<p>These tools are built on a idealised model of cryptography, termed the symbolic model, which requires strong assumptions about the properties of cryptographic primitives. Consequently, automated protocol analyses may miss attacks which rely on properties of real primitives which are missing from the symbolic model. Furthermore, some protocols are not amenable to automated analysis as they use cryptographic primitives for which no suitable symbolic model currently exists.</p>
<p>This motivates natural research questions: How closely does the contemporary symbolic model approximate the real world behaviour of common cryptographic primitives? Can we improve the accuracy and breadth of the symbolic model by developing new approaches to underlying formalism? In this thesis, we set out to address these questions for two popular cryptographic primitives: digital signatures and Diffie-Hellman groups.</p>
<p>The symbolic model of digital signatures was first published nearly two decades ago and is widely used. We uncover a startling mismatch between the standard cryptographic definition of signature scheme security and the symbolic description. We repair this mismatch through the development of a novel symbolic model which we use to discover a number of new attacks on deployed protocols. We also document a number of previous analyses which missed these attacks due to their traditional symbolic model.</p>
<p>Next we consider Diffie-Hellman groups. Unlike digital signatures, symbolic Diffie-Hellman models have evolved considerably in recent years and we review the progress in this area, highlighting two key limitations. Firstly, that these models only describe prime order groups, despite the popularity of non-prime order groups in practice. We develop new symbolic models to remedy this and use them to discover new attacks on real world protocols. Secondly, that there is no effective procedure for analysing protocols which make use of the full field structure of Diffie-Hellman exponents. We develop a new formalism which can be used to mechanically analyse such protocols and demonstrate its effectiveness on hand-worked examples.</p>
<p>Finally, we conclude by examining the methodology behind our approach. We argue that the techniques behind our new symbolic models can be applied to many other cryptographic primitives to yield more accurate symbolic models. We go on to summarise our contributions and sketch several promising lines of future work.</p>
|
|---|