A Formal Methods Analysis of the Session Binding Proxy Protocol

Kirellos N. Abou Elsaad
CSEE Department

Friday, April 1, 2022
Remotely via WebEx: https://umbc.webex.com/meet/sherman

Recording of Talk.


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. This attack is not neutralized by SBP because the request contains a valid session token and is sent over the client’s existing SSL/TLS channel.

About the Speaker:

Kirellos N. Abou Elsaad is a master’s student in computer science at UMBC working under Dr.Sherman and a member of the Protocol Analysis Lab (PAL).

Email: abou3@umbc.edu


Alan T. Sherman, sherman@umbc.edu

Upcoming CDL Meetings:

Apr 15, Edward Zieglar (NSA)
Apr 29, Ian Blumenfeld (UMBC)
May 13, Enka Blanchard (Digitrust Loria, France)


Support for this event was provided in part by the National Science Foundation under SFS grant DGE-1753681.

The UMBC Cyber Defense Lab meets biweekly Fridays 12-1 pm. All meetings are open to the public.