Automatically Binding Cryptographic Context to Messages in Network Protocols Using Formal Methods

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.