Cryptographic Binding Should Not Be Optional: A Formal-Methods Analysis of FIDO UAF Authentication

Abstract: We present a formal-methods analysis of the FIDO Universal Authentication Framework (UAF) authentication protocol, and we present a case study that highlights the pitfalls of optional cryptographic binding by illustrating a man-in-the-middle attack against UAF authentication when cryptographic channel-binding is absent. We carry out our analysis using the Cryptographic Protocol Shapes Analyzer (CPSA) on two significant variations of the protocol: one using the four available channel-binding mechanisms, and one without channel binding. In our case study, we confirm the presence of a harmful protocol interaction in which an adversary, by transferring information from one protocol context to another, can compel a UAF client and authenticator pair to act as confused deputies that help authenticate the adversary to an honest server. Also, we demonstrate the feasibility of such an attack against existing, open-source FIDO implementations, and we suggest potential mitigations. Our work aims to promote the importance of cryptographic binding in mitigating protocol interactions within the Dolev-Yao intruder model to mitigate man-in-the-middle attacks that exploit flaws in a protocol’s structure. Protocol designers and policy makers must be aware that, if cryptographic binding is an optional feature of a protocol standard, then serious vulnerabilities may result. Additionally, we discuss the groundwork for incorporating cryptographic binding into network protocol specifications automatically. Cryptographic binding is a vital tool for resisting adversarial protocol interactions, and many existing and emerging standards, including UAF, do not bind adequately. About the Speaker: Enis Golaszewski (golaszewski@umbc.edu) is a computer science PhD student at UMBC under Alan T. Sherman, where he studies, researches, and teaches cryptographic protocol analysis.