Asymmetric Unification and Indistinguishability
Senior Researcher in Computer Security, Center for High Assurance Systems
Naval Research Office
(Video runs from 00:03:23 to 01:00:38)
In this course we give an overview of the Maude-NPA Protocol Analyzer. Maude-NPA is a tool for the symbolic analysis for cryptographic protocols. It searches for ways in which an active attacker could subvert the protocols' goals, such as authentication or secrecy. Maude-NPA is designed to take account of the algebraic properties of the crypto systems involved, in order to give a more complete representation of both the protocol and the attackers capabilities. In the course of our work in designing Maude-NPA, we have also discovered a number of general techniques and theoretical results that pertain to this problem. These will be discussed in the course as well.
"Asymmetric Unification and Symbolic Indistinguishablity"
In this lecture we discuss two research topics that have risen out of our work with Maude-NPA.
The first, asymmetric unification, is a type of unification with constraints that we found necessary to in order to apply the Maude-NPA state space reduction techniques in a sound manner. It is also used implicitly by most other symbolic cryptographic analysis tools. We show why asymmetric unification is important to symbolic cryptographic protocol analysis, and we describe our research on understanding it better and developing more efficient asymmetric unification algorithms.
The second, symbolic indistinguishability, concerns the problem of developing and reasoning about about symbolic versions of the types of indistinguishability proofs used in cryptography. This allows us to provide a more fine-grained
version of secrecy that is important, for example, for privacy preserving protocols the protect low-entropy data.
Thus it is an active topic of research in symbolic cryptographic protocol analysis. We describe our research in the development of a version of symbolic indistinguishability that captures the notion in an intuitive way and can be expressed in terms of equational theories.
Catherine Meadows 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 a large number of protocols, including the Internet Key Exchange Protocol and the Group Domain of Interpretation protocol, both of which became standards for the Internet Engineering Task Force.
Currently she is co-PI on a project that is developing a successor to the NRL Protocol Analyzer, Maude-NPA, that takes into account complex algebraic properties of cryptosystems. Other research efforts she is or has been involved in recently with include the machine-verified analysis of crypto-algorithms and protocols for the IARPA-sponsored Security and Privacy Assurance Research Program, the development of automated methods for the generation and analysis of crypto systems, and the development of logical methods for reasoning about security procedures that involve the cooperation of humans and devices. Prior to joining NRL, she was on the mathematics faculty at Texas A&M University. There she worked in various areas of cryptography, including secret sharing schemes and software protection. She received her Ph.D. in mathematics from the University of Illinois at Urbana-Champaign.