Model Checking for Security Protocols,

Abstract

As more resources are added to compiler 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 modeling circuits as finite state machines and examining all possible execution traces modeling 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.

Keywords

This publication has 0 references indexed in Scilit: