Model checking a security protocol.
Acknowledgement
The following case study has been adapted from
a similar one done in murphi.
PROTOCOL'S DESCRIPTION
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
RESULTS
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
step-comments@cs.stanford.edu
Last modified: Sat Aug 8 19:39:55 PDT 1998