SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Protocol Specification and Analysis in Maude
 by Dr. Grit Denker, Dr. Carolyn Talcott & Josť Meseguer.

This paper proposes rewriting logic as an executable specification formal ism 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 [CELM96] 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 be comes 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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy