[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Protocol Specification and Analysis in Maude
Denker, G. and Meseguer, J. and Talcott, C. L. - 1998

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 \citeClaEkeLin96 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 \em 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.