Unification and Narrowing in Security Applications
Associate Professor, School of Engineering in Computer Science
Universitat Politècnica de València, Spain
(Video runs from 00:30:18 to 01:42:58)
Narrowing was originally introduced to solve equational unification problems. It is also the key mechanism to unify functional programming and logic programming into one paradigm, functional-logic programming. In this case, an equational theory is assumed to be represented as a set of terminating, confluent, and coherent set of oriented equations modulo some other equational properties called axioms. Under these assumptions, we have developed an evaluation strategy, called folding variant narrowing, that improves existing techniques in several ways, providing equational reasoning, for example, to obtain an effective equational unification algorithm.
A rewrite theory extends an equational theory with extra behaviours. Such rewrite theories axiomatize concurrent systems, whose states are equivalence classes of terms modulo the equational theory, and whose transitions are specified by transition rules (possibly non-terminating and non-deterministic rewrite rules). Under these assumptions, a much wider range of analysis techniques is possible: from standard reachability to symbolic reachability and from model checking to logical model checking. A concrete example of the use of narrowing is the Maude-NPA cryptographic protocol analysis tool, both for symbolic reachability and for equational unification.
Furthermore, security applications such as cryptographic protocol analysis include specific requirements that can be exploited during symbolic reachability. We have extended the symbolic reachability framework to include irreducibility constraints, which are common to communication processes and appear normally during analysis and verification.
Santiago Escobar is associate professor at the Universitat Politècnica de València (UPV), Spain. His research interests include formal methods, security, verification, model checking, rewriting, narrowing, and evaluation strategies. His works on narrowing have been discovered to be essential for narrowing-based applications such as equational unification, model checking, or protocol analysis. In the security area, he has developed the Maude-NPA cryptographic protocol analyzer in collaboration with Catherine Meadows from the Naval Research Laboratory of Washington D.C. and Jose Meseguer from the University of Illinois at Urbana-Champaign. This is the state-of-the-art tool for verification of protocols with advanced cryptographic properties. He has published more than 60 papers on conferences and journals on formal methods, verification, and security. He has been program chair of specialised workshops on unification (UNIF 2012), reduction strategies (WRS 2011), functional and (constraint) logic programming (WFLP 2009), automated specification and verification of web systems (WWV'07&08), and security and rewriting (SecReT'08). Dr. Escobar received a M.Sc. in 1998 and a Ph.D. in Computer Science in 2003 at the Universitat Politècnica de València.