next up previous
Next: Related Work Up: A Model Checker for Previous: A Model Checker for

Introduction

Security for early computers was provided by their physical isolation. Unauthorized access to these machines was prevented by restricting physical access. The importance of sharing computing resources led to systems where users had to authenticate themselves, usually by providing a name/password pair. This was sufficient if the user needed to be physically at the console or was connected to the machine across a secure link. However, the efficiency to be gained by sharing data and computing resources has led to computer networks, in which the communication channels cannot always be trusted. In this case, authentication information such as the name/password pairs could be intercepted and even replayed to gain unauthorized access. When such networks were local to a certain user community and isolated from the rest of the world, many were willing take this risk and to place their trust in the community. However, in order to be able to share information with those outside the community, this isolation would have to be removed. The benefits to be had by such sharing have been enormous, and the gains are demonstrated by the growth of such entities as the Internet and the World Wide Web. Now, very few, if any guarantees can be made about the communication links. Numerous protocols that take advantage of cryptography have been proposed that claim to solve many of the security issues. The correctness of these protocols is paramount, especially when we consider the size of the networks involved and the desire of users to place confidential information and to allow for monetary transactions to take place across these networks.

Typically, these protocols can be thought of as a set of principals which send messages to each other. The hope is that by requiring agents to produce a sequence of messages, the security goals of the protocol can be achieved. For example, if a principal A receives a message encrypted with a key known only by principals A and B , then principal A should be able to conclude that the message originated from principal B . However, it would be incorrect to conclude that principal A is talking to principal B . An adversary could be replaying a message overheard during a pervious conversation between A and B . So, depending on the security goal of this simple example protocol, the protocol may or may not be secure. Because the reasoning behind the correctness of these protocols can be subtle, a number of researchers have turned to formal methods to prove protocols correct.

In order to concentrate on the security of the protocol itself as opposed to the the security of the cryptosystem used, the vast majority of research in this area has made the following ``perfect encryption'' assumptions.

While the assumptions are obviously not true, they are, in practice, reasonable. They are important because they allow us to abstract away the cryptosystem and analyze the protocol itself. In particular, if there is an attack on this abstracted protocol, then the same attack exists when a real cryptosystem is used.


next up previous
Next: Related Work Up: A Model Checker for Previous: A Model Checker for