Automatically Binding Cryptographic Context to Messages in Network Protocols Using Formal Methods

Abstract

Using formal methods, we identify and correct the failure of cryptographic network protocols to establish explicit session contexts and cryptographically bind their messages to these contexts. To characterize this failure, we formally analyze two protocols, Session Binding Proxy (SBP) and the FIDO Universal Authentication Framework (UAF), in the strand space model. We then apply lessons learned from our analyses to devise an automatic method by which two communicants, engaging in an arbitrary two-party protocol, agree on a final session context. First, we analyze SBP, which protects a vulnerable system by wrapping it and introducing a reverse proxy between the system and its clients. SBP mitigates thefts of authentication cookies by cryptographically binding the authentication cookie---issued by the server to the client---to an underlying Transport Layer Security (TLS) channel using the channel's master secret and a secret key known only by the proxy. Our analysis verifies that the original SBP design mitigates cookie stealing under the client's cryptographic assumptions but fails to authenticate the client to the proxy. Next, we analyze UAF's cryptographic channel binding mechanisms. First, we show that UAF's channel bindings fail to mitigate protocol interaction by a Dolev-Yao (DY) adversary, enabling the adversary to transfer the server's authentication challenge to alternate sessions of the protocol. Second, we implement a proof-of-concept man-in-the-middle attack against eBay's open source FIDO UAF implementation. Third, we propose and verify an improvement of UAF channel binding that better resists protocol interaction, in which the client and the server, rather than the client alone, bind the server's challenge to the session. Finally, we present an automatic method to bind arbitrary two-party protocols to unique cryptographic sessions by binding the original protocols to cryptographic session contexts, alongside a technique for proving security properties of the augmented protocols automatically. Cryptographic session contexts are hashes that incorporate identities of each communicant, fresh nonces from each communicant, all introduced session variables, or session variables that appear in messages, and protocol descriptors such as the protocol name, version, and message identifiers. To construct the final session context, communicants complete a session context exchange protocol, which we generate using our automatic method and interleave with messages of the original protocol. When evaluated against two examples---Needham-Schroeder (NS) and Blanchet's Simple Protocol (BSP)---our transformation provably eliminates protocol interactions between sessions of the transformed protocols in the DY model.