Limitations of Wrapping Protocols and TLS Channel Bindings: Formal-Methods Analysis of the Session Binding Proxy Protocol
摘要
We present the first formal-methods analysis of the Session Binding Proxy (SBP) protocol, which mitigates theft of a server-issued authentication cookie from a client communicating with a vulnerable, legacy server. To protect the cookie, SBP cryptographically binds the cookie to an underlying Transport Layer Security (TLS) channel using the channel’s master secret and a secret key known only to a reverse proxy, which SBP introduces between the server and the client. An adversary who steals the bound cookie cannot reuse this cookie to create malicious requests on a separate connection because the cookie’s channel binding will not match the adversary’s channel. Because SBP does not modify the client or server software, it renders the client and server “oblivious protocol participants” that are not aware of the SBP session. Our analysis verifies that SBP mitigates cookie theft under the client’s cryptographic assumptions but fails to authenticate the client under the proxy’s assumptions: the proxy lacks assurance that the client generates a fresh TLS pre-master secret, and the legacy server relies on usernames and passwords to authenticate the client. Our analysis of this obscure protocol sheds insight into the role and limitations of TLS channel bindings when augmenting legacy protocols.