[Distinguished Seminar] Crypto Protocol Analysis with Time and Space
Wednesday, November 2, 2022
11:00 am - 12:00 pm
Speaker
Dr.
Catherine
Meadows
Center
for
High
Assurance
Systems
at
the
Naval
Research
Laboratory
(NRL)
Location
PGH 232
Abstract
With the advent of the Internet of Things, it is becoming increasingly necessary to secure the interactions of devices through cryptographic protocols, not only to provide secrecy and authentication of the communications, but to provide verification of location and presence of devices. With this in mind, we present a formal framework for the analysis of cryptographic protocols that make use of time and space in their execution. This time and space protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time and space information are not represented by specific values but by logical variables, and in which the properties of time and space are reasoned about in terms of constraints on those time and space logical variables. All the time and space constraints are carried along the symbolic execution of the protocol, and their satisfiability can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be rejected as impossible.
We demonstrate the feasibility of our approach by using the Maude-NPA symbolic cryptographic protocol analyzer, together with an SMT solver that is used to evaluate the satisfiability of timing and location constraints. We provide a sound and complete protocol transformation from our time and space process algebra to the Maude-NPA syntax and semantics. We also demonstrate the tools’ performance on two protocols, one for proximity verification, and one for secure localization, and show what we have been able to accomplish with this approach, as well as avenues for future research.
About the Speaker
Catherine Meadows received her Ph.D. in mathematics from the University of Illinois at Urbana-Champaign. She is a senior researcher in computer security at the Center for High Assurance Systems at the Naval Research Laboratory (NRL), heading that group’s Formal Methods Section. She was the principal developer of the NRL Protocol Analyzer (NPA), which was one of the first software tools to find previously undiscovered flaws in cryptographic protocols, and has been used successfully in the analysis of protocol standards. The techniques developed for NPA have been incorporated and expanded in the Maude-NPA tool, for which, together with Jose Meseguer and Santiago Escobar, she serves as a co-designer of the tool. She has also worked on the designing and analyzing different types of security solutions and protocols, including secure multicast, secure multiparty computation, geolocation protocols, and communication through covert channels, and as well as developing techniques for analysis of cryptographic algorithms using symbolic methods.
Host
Dr. Rakesh Verma
