Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA
Abstract
Several extensions to protocol analyzer are considered. First, equational unification is just a subfield of another vast area of research called satisfiability modulo a theory (SMT). Anyone who has solved a set of arithmetic inequations such as x + 7 = 12 + y ^ x 3 ^ y 5 ^ x 6= y has reasoned about formula satisfiability, where x = 5 ^ y = 0 is one possible solution. The differences between unification and SMT are, basically, that SMT considers formulas beyond equalities (disequalities, inequalities, etc.) and that we are not interested in finding all solutions but knowing whether there is at least one possible solution. There has been a growing interest in extending protocol analyzers to reason about properties of different data structures, e.g., discrete and dense time, and SMT technology is the best bet. Early attempts in integrating SMT into protocol analyzers did not consider satisfiability modulo algebraic properties (only boolean formulas). Second, in the same way equational unification concentrated on theory-specific algorithms rather than theory-generic algorithms, SMT suffers from the very same problem but it is even more bleeding, since there is no clear whatsoever theory-generic approach. Developing theory-generic SMT approaches and integrating them into protocol analyzers would increase their applicability. Third, although there are many interesting cryptographic theories that satisfy the conditions for theory-generic equational unification in Maude, there is a class of equational theories that appears prominently in cryptographic protocols applied to privacy-preserving computation: operators that are homomorphic with respect to another, e.g., q(X Y ) = q(X) q(Y ), or that satisfy some distributivity law e.g., X (Y + Z) = (X Y ) + (X Z). Developing equational unification algorithms for this class of theories would expand the possibilities of several protocol analyzers, both at the unification and satisfiability level
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jul 28, 2017
- Source ID
- FA95501710286
Entities
People
- Santiago Escobar-romain
Organizations
- Air Force Office of Scientific Research
- Technical University of Valencia
- United States Air Force