Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a state-transition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications.

In this lecture, we describe the basic model checking algorithm and show how it can be used with binary decision diagrams to verify properties of large state-transition graphs. We also discuss how techniques based on abstraction, compositional reasoning and symmetry can be used to extend the power of the basic algorithm to handle extremely complex reactive systems.

A Model Checker for Security Protocols

As more resources are added to computer networks, and as more vendors look to the World Wide Web as a viable marketplace, the importance of being able to restrict access and to insure some kind of acceptable behavior even in the presence of malicious adversaries becomes paramount. Researchers have looked to cryptography to help solve many of these problems. However, cryptography itself is only a tool. The security of a system depends not only on the cryptosystem being used, but also on how it is used. Typically, researchers have proposed the use of security protocols to provide these security guarantees. These protocols consist of a sequence of messages, many with encrypted parts. In this paper, we develop a method of verifying these protocols using a special purpose model checker. Model checking has proven to be a very useful technique for verifying hardware designs. By modelling circuits as finite-state machines, and examining all possible execution traces, model checking has found a number of errors in real world designs. Like hardware designs, security protocols are very subtle, and can also have bugs which are difficult to find. Because a model of a protocol is necessarily an abstraction, we cannot prove a protocol correct. However, because we perform an exhaustive search, our tool is extremely useful as a debugger. We have used our tool to analyze 14 different authentication protocols, and have found the previously reported attacks for them.

Joint research with Will Marrero and Somesh Jha.