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

Abstract:

We present an automatic method that binds any two-role protocol to an underlying unique cryptographic context. Our method eliminates a large class of adverse protocol interactions (e.g., man-in-the-middle attacks) and facilitates proving authentication properties of the transformed protocol automatically. We transform the original protocol by combining it with a context-exchange protocol, in which the initiator and the responder collaborate to construct a cryptographic context for the original protocol. Represented as a Merkle hash tree, the cryptographic context comprises protocol parameters, session parameters, and fresh nonces. Each party signs the context. To complete the transformation, we interleave messages of the context-exchange protocol with the original protocol’s messages. We then generate authentication security goals, which we verify automatically using the Cryptographic Protocol Shapes Analyzer (CPSA). To illustrate our method, we transform two flawed examples, Needham-Schroeder (NS) and Blanchet’s Simple Protocol (BSP), and prove that our method corrects each protocol in the Dolev-Yao (DY) adversarial model. Our method does not alter the message structure of the original protocol and does not require the original protocol to have any particular security properties. The transformed protocol requires each original message to include an encrypted hash and a fresh nonce, adds an extra message, and computes hashes and encryptions that scale linearly with the number of protocol steps.

Support for this research was provided in part by the National Security Agency under an INSuRE+C grant via Northeastern University.

About the Speaker:

In May 2024, Enis Golaszewski ([email protected]) completed his PhD in computer science at UMBC under Alan T. Sherman, where he researches and teaches cryptographic protocol analysis.