Protocol Specification and Analysis in Maude

This paper proposes rewriting logic as an executable specification formalism for security protocols that offers some novel advantages. A message-passing object-oriented approach seems particularly natural for communication protocols and can be naturally formalized in rewriting logic. This is illustrated by using the Needham-Schroeder Public-Key protocol as a running example. The rewriting logic-based Maude interpreter offers also some useful advantages. Efficient executability allows prototyping and debugging of protocol specifications. But since a concurrent system can have many different behaviors, to properly analyze the system it becomes important to explore not just the single execution provided by some default strategy, but many other executions. Maude supports user-defined execution strategies, including strategies such as breadth-first-search that can exhaustively explore all the executions of a system. This is very helpful in uncovering security flaws under unforeseen attack scenarios such as those found for NSPK. We also discuss future developments along of this work, including (1) narrowing using symbolic execution techniques, (2) modularity and compositionality issues in formal reasoning, and (3) combination of rewriting logic and temporal logic.