Professor Mitchell presented a project he had worked on, named Murj (difficult to typeset), a method by which cryptographic protocols can be analyzed for errors. His reason for discussing something that was not, say, straight along the lines of programming theory was that he had much more fun starting questions, as with Murj , than finishing them up. He had also just finished a big book.
A protocol, Mitchell outlined, is something which can be as small as a three-line program agreed upon for communicative compatibility. Cryptographic protocols are used to communicate over an insecure network (just about unavoidable) and use cryptography to achieve the goal of security. The automated analysis of these protocols involves testing them on a bound number of steps, a finite number of parties, and with a non-deterministic adversary who basically tries to screw it up and violate the security.
The centerpiece example Mitchell used to illustrate the effectiveness of Murj and the possibility of loopholes in the most established of cryptographic protocols was the Needham-Schroeder key exchange. The exchange is a methodology through which information is supposedly passed between two parties with 100% assurance about the validity of the data and who the receiver is and who the sender is.
The first thing to know when discussing security, Mitchell noted, was about Alice and Bob, or A and B, the two universal parties. The second thing necessary to understanding the N-S exchange is the use of public encryption and private decryption keys. This means that anyone can learn of and use a specific key to encode information, but only one person can decode that information. The public decryption key can be put on the person's home page, for example, for other people to use to send secure messages which can only be understood by that person. The third ingredient is for each party to pick a secret number which would be nearly impossible to guess given one chance. The secret number is sent as part of the message for added security.
The diagram of the exchange is as follows, and I will quickly summarize what it means:
A is for Alice, and in the first message, Alice sends her name to let Bob know the message is from her. Nx represents a secret number, where X is who originated the number. Kx is whose public decryption key is used.
The reason why this seems infallible is due to three possible actions that a third party adversary can make. 1) Block the message. 2) Substitute one of the messages with a fake. 3) Decrypt a message. We assume 3) is impossible. If a message is blocked, then the system still holds its integrity because neither party is fooled; they understand the communcation has not completed and are not satisfied. If a message is substituted, the system still holds because the substitution would assumably entail a secret number different from the one chosen by the actual party. Thus if Alice in Bob's reply sees a different number than the one sent out, she knows the communication has been corrupted. Likewise for Bob's last reception from Alice.
However, it wasn't until 20 years after the design of the Needham-Schroeder exchange that a flaw was found, as is explained in this diagram, which you can decipher for yourself:
Poor Bob is fooled, and evil Eve has stolen Bob's secret number. The solution, as mindbogglingly simple as it is, is for Bob to simply include his name in his first return transmission.
Where it took 20 years of just sitting around and thinking about it to discover the flaw in the exchange, it took Murj 1.7 seconds. So what is Murj ? Murj describes a finite state system, and non-deterministically tries to find an error in the automata using an adversary that controls the network and tries to interfere with the state transitions. That's the simplistic description.
Murj performs at least as well as other similar tools. The N-S exchange, Kerberos, and the TMN cell phone protocol are some examples of where Murj has found bugs. There are limitations to Murj , however. The adversary must be manually formulated for one, which is time consuming and has potential for errors. The paradigm also ignores probabilistic factors, and shies from great complexity.
But in the end, Professor Mitchell stated, Murj can perform at least as well as a bunch of people sitting around thinking about the problem. And if you can get your computer to act enough like a smart person, and thus save you time for the beach, you're okay.