Model checking a security protocol.


The following case study has been adapted from a similar one done in murphi.


Briefly, the Needham-Schroeder protocol [1978] allows two agents A and B to exchange two secret nonces. Initiator A choose at random a nonce Na, and sends it with its address to responder B, encrypting the message with B's public key Kb:
   (1)   A --> B:  {Na, A}Kb
Responder B decrypts the message and acquires knowledge of Na. Then he chooses at random a nonce Nb, and sends both Na and Nb to A, using A's public key Ka for the encryption:
   (2)   B --> A: {Na, Nb}Ka
Now A is certain of the authenticity of B, since only B could decrypt the first message of the protocol. The protocol ends with a message from A to B, containing Nb, and encrypted with Kb
   (3)   A --> B: {Nb}kb
Now A should be correctly authenticated, but this is not the case! Refer to Lowe [1996] to discover why. Here we just say that, according to Lowe, the protocol may be fixed in this manner:
   (1)   A --> B:   {Na, A}Kb
   (2)   B --> A:   {Na, Nb, B}Ka
   (3)   A --> B:   {Nb}Kb 


                   responder          initiator
                   correctly          correctly
                   authenticated      authenticated
ns1.fts         |  holds          |   does not hold
weak-ns1.fts    |  holds          |   does not hold
ns2.fts         |  holds          |   holds
Advice: run SMC, go to take a coffee, and when you will return STeP will say you if the property holds or does not. If the property does not hold you will also be given a counterexample
Last modified: Sat Aug 8 19:39:55 PDT 1998