Lecture 7 (Wed 10/29/97)

Scribe: Dawn Song

Part I -- Model Checking A model checker for security and cryptography provides an messages exchanging and flowing environment. It includes an adversary which can eavesdrop all the messages and can send messages. With keys, the adversary can encrypt messages and decrpt messages. It can also keep track of the things it has seen, like nonces and keys.

Here we discuss two model checkers: Mur-phi(Stanford Univ) and FDR.
Both Mur-phi and FDR are nondeterministic finite state machine. They have similar adversary description and both do enumeration. They can not deal with large amount of participants, because states will explode. FDR is a little more abstracted and high level than Mur-phi.

To use Mur-phi, first we need to formulate the portocols and then state the desired correctness condition and then run the protocol. To use FDR, we model the protocols in CSP(communication gsequential processes), using sets to describe the protocols(initiator, responder, key, nonces) and check the protocols via processes.

Both of the two model checkers have found all bugs in protocols tested in an acceptable time. But so far, they can only prove something is wrong but not prove something is correct.

Part II -- Model Checking (Will Marrero) Difference between theorem prover and model checker in security and cryptography is that : theorem prover tries to prove the property and has no guarantee for termination, while model checker is searching for flaw in finite steps , so guarantee for termination. Both of the two methods get more complicated when the protocol get bigger. So far, no model checker has dealt with more than 2 simultaneous runs. Because when the number of simultaneous runs gets bigger, the number of states will increase almost exponentially which will explode very soon.