A Model Checker for Authentication Protocols

Will Marrero - Edmund Clarke - Somesh Jha

Abstract:

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 intruders becomes paramount. People 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 way of verifying these protocols using model checking. 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. By examining all possible execution traces of a security protocol in the presence of a malicious intruder with well defined capabilities, we can determine if a protocol does indeed enforce its security guarantees. If not, we can provide a sample trace of an attack on the protocol.