A Formal Methods Analysis of the Session Binding Proxy Protocol

Abstract

Proposed by Burgers, Verdult, and Eekelen in 2013, the Session Binding Proxy (SBP) protocol intends to prevent session hijacking by binding the application session to the underlying network session (i.e., binding the session token to the SSL/TLS shared key). We present a formal methods analysis of SBP using the Cryptographic Protocol Shapes Analyzer (CPSA). Our analysis reveals that SBP relies critically on the successful establishment of a secure SSL/TLS channel, which can be undermined using well-known attacks. Also, we find that SBP allows for the partial hijacking of a session using a tailgating attack. In this attack, the adversary uses the server to inject and execute malicious code inside the client’s browser to extract the session token and forge a valid state-changing request to the server. SBP does not neutralize this attack because the request contains a valid session token and that is sent over the client’s existing SSL/TLS channel. The informal security analysis conducted by the originator of SBP failed to consider these attacks. To our knowledge, our work is the first formal methods analysis of SBP.