Enis Golaszewski
CSEE Dept., UMBC
12 pm – 1 pm
Friday, December 1, 2023
Remotely via WebEx: https://umbc.webex.com/meet/sherman
Abstract:
We present an automatic tool for binding formal network protocol specifications to their underlying cryptographic contexts, eliminating harmful protocol interactions, including Man-in-the-Middle (MitM) attacks. Operating in the strand space model, our tool takes as input an arbitrary two-party protocol specification, infers a cryptographic context from the protocol terms, and outputs a specification for an improved protocol that is the composition of the input protocol and our novel context-exchange protocol. Our context-exchange protocol binds cryptographic values to a unique session, using a Merkle hash tree to represent context. Our tool applies the following operations on context: initialize, append, sign, and verify. For each input protocol specification, our tool outputs context-equivalence security goals, which we then verify using the Cryptographic Protocol Shapes Analyzer (CPSA). To our knowledge, our tool is the first of its kind. It represents a significant step towards eliminating attacks resulting from unwanted protocol interactions, which are the cause for most known structural weaknesses in protocols.
Support for this research was provided in part by the National Security Agency under an INSuRE+C grant via Northeastern University.
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:
- January 16-19, 2024, UMBC SFS/CySP Research Study
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.