Detecting the misuse of secrets: foundations, protocols, and verification

Secrets are the basis of most protocol security, enabling authentication and secrecy over untrusted channels even in the presence of active adversaries. The compromise and misuse of secrets can therefore undermine the properties that people and systems rely on for their security. In this thesis, we develop foundations and constructions for security protocols that can automatically detect, without false positives, if a secret such as a key or password has been misused. These constructions allow protocol participants to automatically trigger an appropriate response and minimize the effects of compromise. Our threat model includes malicious agents, (temporarily or permanently) compromised agents, and clones. Unlike existing approaches to detection, for which designs are interwoven with domain-specific considerations and which usually do not enable fully automatic response (i.e., they need human assessment), our approach makes it clear where automatic action is possible. Our results unify, justify the design of, and suggest improvements for existing domain-specific solutions. For example, we propose an improvement to Cloudflare's Keyless SSL protocol that enables key misuse detection, and a modified ISO-IEC 9798 protocol for use in high-security smart-card applications such as the Common Access Card. Our results show that protocols which detect misuse must be stateful. Although stateful protocols are becoming more common, formally analyzing them remains a challenge. We develop and implement several improvements to the Tamarin prover to alleviate this difficulty, and use them to formally verify our proposed detection protocols. We demonstrate the wide applicability of our improvements to Tamarin by analyzing several real-world protocols. Notably, we perform the first full formal analysis of both WireGuard, and the DNP3 Secure Authentication protocol---a complex multi-stage stateful protocol used to authenticate critical monitor and control functionality in SCADA systems.