Lambda the Ultimate

Ross Anderson and Roger Needham, 1995. Programming Satan’s Computer. In J. van Leeuwen, editor, Computer Science Today, LNCS 1000, pages 426-440.

Cryptographic protocols are used in distributed systems to identify users and authenticate transactions. They may involve the exchange of about 2–5 messages, and one might think that a program of this size would be fairly easy to get right. However, this is absolutely not the case: bugs are routinely found in well known protocols, and years after they were first published. The problem is the presence of a hostile opponent, who can alter messages at will. In effect, our task is to program a computer which gives answers which are subtly and maliciously wrong at the most inconvenient possible moment. This is a fascinating problem; and we hope that the lessons learned from programming Satan’s computer may be helpful in tackling the more common problem of programming Murphy’s.

Incidentally, the first edition of Anderson's book, Security Engineering, Wiley, 2001, is available for download.