Formal analysis of modern security protocols in current standards

Thesis

While research has been done in the past on evaluating standardised security protocols, most notably TLS, there is still room for improvement. Modern security protocols need to be rigorously and thoroughly analysed, ideally before they are widely deployed, so as to minimise the impact of often creative, powerful adversaries. We explore the potential vulnerabilities of modern security protocols specified in current standards, including TLS 1.2, TLS 1.3, and SSH. We introduce and formalise the threat of Actor Key Compromise (AKC), and show how this threat can and cannot be avoided in the protocol design stage. We find AKC-related and other serious security flaws in protocols from the ISO/IEC 11770 standard, find realistic exploits, and harden the protocols to ensure strong security properties. Based on our work, the ISO/IEC 11770 working group is releasing an updated version of the standard that incorporates our suggested improvements. We analyse the unilaterally and mutually authenticated modes of the TLS 1.3 Handshake and Record protocols according to revision 06 of their specification draft. We verify session key secrecy and perfect forward secrecy in both modes with respect to a powerful symbolic attacker and an unbounded number of threads. Subsequently, we model and verify the standard authenticated key exchange requirements in revision 10. We analyse a proposal for its extension and uncover a flaw in it, which directly impacts the draft of revision 11.

Authors: Horvat, M

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Keywords: actor key compromise; KCI; AKC; IEC; TLS; security standards; security protocols; standardisation; ISO; IETF
• Subjects: Formal methods; Symbolic verification; Formal verification; Security protocols