Introduction

This webpage is a repository of publications and examples related to security protocol analysis using Murphi and model checking in general.

About Murphi

The Murphi verification system is a finite-state machine verification tool. The purpose of finite-state analysis, commonly called "model checking", is to exhaustively search all execution sequences. While this process often reveals errors, failure to find errors does not imply that the protocol is completely correct. To use Murphi for verification, one has to model the protocol in the Murphi language and augment this model with a specification of the desired properties. The Murphi system automatically checks, by explicit state enumeration, if all reachable states of the model satisfy the given specification. For more information visit the Murphi homepage.

Contact