Formal-Methods Analysis of the Session Binding Proxy Protocol: Advantages and Dangers of Oblivious Protocol Participants

Enis Golaszewski
PhD Student
CSEE Dept, UMBC

12:00pm (noon) – 1pm
Friday, September 29, 2023
Remotely via WebEx: https://umbc.webex.com/meet/sherman

Joint work with Alan T. Sherman, Edward Zieglar, and Kirellos Abou Elsaad

Recording of Talk

Abstract:

We present a formal-methods analysis of the Session Binding Proxy (SBP) protocol, in which we highlight the advantages and dangers of an oblivious protocol participant: an unaware web server residing behind an SBP reverse-proxy. We carry out our analysis using the Cryptographic Protocol Shapes Analyzer (CPSA) on three deployment variations of SBP: a server that embeds a proxy, a stand-alone proxy on a private network, and a stand-alone proxy on a public network. Our analysis reveals fundamental issues affecting oblivious protocol participants in a Dolev-Yao (DY) network: to mitigate adversarial protocol interactions, deployments of SBP must ensure that the server authenticate and communicate exclusively with a legitimate proxy by establishing a private communication channel, deploying mutual authentication such as mutual Transport Layer Security (mTLS), or embedding the proxy with the server.

Our work identifies benefits and risks of wrapper protocols such as SBP, which wrap existing legacy or third-party systems to mitigate known vulnerabilities. Additionally, we identify minimal requirements for cryptographic binding, a vital tool for resisting protocol interactions, implement a “tailgating” attack on SBP, and discuss the pitfalls of ad-hoc, overly constrained adversarial models.

About the Speaker:

Enis Golaszewski (golaszewski@umbc.edu) is a computer science PhD student at UMBC under Alan T. Sherman, where he studies, researches, and teaches cryptographic protocol analysis.

Host:

Alan T. Sherman, sherman@umbc.edu

Upcoming CDL Meetings:

  • October 6, RJ Joyce (UMBC), Benchmarks datasets for Malware
  • October 20 (1-2pm) Josh Benaloh (Microsoft), ElectionGuard
  • November 3, Jason Rheinhart (Sandia), Risk analysis
  • November 17 (1-2pm) Austin Murdoch (Sixmap)
  • December 1, Enis Golaszewski (UMBC), Automatic cryptographic bindings

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.