Introduction to Maude-NPA
Senior Researcher in Computer Security, Center for High Assurance Systems
Naval Research Office
(Video runs from 27:23 to 1:33:40)
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.
"An Introduction to Maude-NPA"
In this talk we describe the basic principals behind Maude-NPA, show how it handles equational theories describing cryptosystems, and describe its rewriting-based semantics and implementation. If time permits, we will also show how composition protocols is handled in Maude-NPA.
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.