Researchers tackle the gap between secure cryptographic design and buggy code

<p>Modern computer systems communicate using protocols. Protocols are critical to security as they are the interface over which systems are accessible to the outside world. Cryptography is what enables secure communication even over insecure channels, and cryptographic protocols are the basis for modern internet security. Encryption enables confidentiality even if eavesdropping is possible, and cryptographic signatures can provide authenticity even if messages can be mimicked, modified, or reproduced.</p><p>Designing secure cryptographic protocols remains challenging. Many protocols once believed to be secure have since been broken and redesigned. The highest guarantees of security are achieved using formal methods, where mathematical logic is used for reasoning. Modern formal methods research tools have proven effective in finding and proving the absence of flaws in protocols, yet they are challenging to use. Correctly implementing large, complex protocols is also a challenge, and many vulnerabilities have been caused by errors introduced during the implementation phase. Formal software verification remains a daunting task which often requires manual effort by formal methods experts.</p><p>This licentiate thesis contributes towards providing formal protocol analysis methods that are intended to be more practical and useful for industrial application. Both the design phase of protocols and the analysis of protocol implementations are covered, showing how modern tools can be used to perform thorough analysis. The analysis discovers design and implementation flaws in modern commercial cryptographic protocols which are reported to the developers.</p><p>The analysis demonstrates challenges as well as the opportunities of adopting more formal methods for the analysis of protocols. Challenges which are tackled in this thesis include specifying an accurate model and selecting security properties for remote attestation proto-cols, and circumventing state space explosion during symbolic execution of protocol implementations. Opportunities include the ability to provide a more thorough analysis of protocol specifications as well as implementations in order to cover requirements which are difficult to test.</p><p>To make verification goals and assumptions more clear, this thesis also presents precise formulations of authentication which are appropriate for verification in the formal model. The authentication properties are suitable for protocols which perform one-way authentication of one of the agents, and complement existing mutual authentication definitions.</p>