talk: Formal Methods Analysis of the Session Binding Proxy Protocol, 12-1 Fri 4/1

The UMBC Cyber Defense Lab presents

A Formal Methods Analysis of the Session Binding Proxy Protocol

Kirellos N. Abou Elsaad, UMBC

12-1 pm, Friday, 1 April 2022, via WebEx

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.

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

Host: Alan T. Sherman, sherman@umbc.edu. 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. Upcoming CDL Meetings: April 15, Edward Zieglar (NSA); April 29, Ian Blumenfeld (UMBC); May 13, Enka Blanchard (Digitrust Loria, France).

• More Information about talk: Formal Methods Analysis of the Session Binding Proxy Protocol, 12-1 Fri 4/1