Analysis of cryptographic protocols

We formulate each participant in the cryptographic protocol as an ASTRAL process instance, which are generally users, key server(s) and intruder. We integrate the network with the intruder as one process in the sense that the intruder will control the network and each participant communicates with others via the intruder. In this way, the intruder can overhear, delete, or store each message and generate new messages by using his knowledge of overheard messages. For users (as well as the key server) the transitions in the process include sending messages, receiving messages, and generating nonces (or session keys). For the intruder, on the other hand, the transitions include storing (overhearing) messages, relaying messages, generating nonces, and attacking other honest participants by placing malicious messages into the network. So, in our model, the intruder plays three roles: a legitimate user, a spy, and the network.

Needham-Schroeder Public Key Protocol

The Needham-Schroeder Public Key Protocol serves to exchange nonces between the initiator and the responder using public keys for mutual authentication. The full protocol has seven steps as follows:

1. $A\to S: A,B$

2. $S\to B: \{K_b,B\}_{K_s^{-1}}$

3. $A\to B:\{N_a,A\}_{K_b}$

4. $B\to S: B,A$

5. $S\to B:\{K_a,A\}_{K_s^{-1}}$

6. $B\to A:\{N_a,N_b\}_{K_a}$

7. $A\to B:\{N_b\}_{K_b}$

By assuming that each participant already knows all the public keys, we can simplify the protocol into 3 messages:

1. $A\to B:\{N_a,A\}_{K_b}$

2. $B\to A:\{N_a,N_b\}_{K_a}$

3. $A\to B:\{N_b\}_{K_b}$

To initiate the protocol, initiator A generates a nonce $N_a$, encrypts it with its own ID under responder B' s public key $K_b$ and sends it to B . Then B knows $N_a$ by decrypting the message, and generates a nonce $N_b$, encrypts $N_b$ with $N_a$ under A' s public key $K_a$. When A receives the second message, A knows that B got the initial message by comparing the nonce $N_a$ in these two messages. After A sends the last message to B , in the same way, B authenticates A .

The ASTRAL specification of the protocol is in the appendix. The processes ProcessInitiator and ProcessResponder perform the message passing described in the protocol via the intruder process, ProcessIntruder. ProcessIntruder, serves as the network and the intruder, has legitimate status, can either perform legal activities such as initiating, sending and receiving messages allowed by the protocol, relaying messages to other participants, or maliciously producing messages by combining nonces, keys, and user_ids it knows. The knowledge of the intruder is held in its local variables:

         know_nonce_a(PID):Integer,
         know_nonce_b(PID):Integer

where, as shown in the protocol, two nonces play different roles when the intruder can wisely use them. In addition,

         ifknow_nonce_a(PID):Boolean,
         ifknow_nonce_b(PID):Boolean,

are Boolean variables indicating if the intruder knows the nonce. Though for efficiency, we will not explicitly encrypt each message, the entry condition shows that only if the message is encrypted under the intruder's own public key, does the intruder know the content of the message, otherwise, it can only store, relay or delete it.

The intruder can arbitrarily delay any messages at will by putting nonsense messages on the network that other honest participants will never acknowledge. The timing condition is not critical in this specification though we put duration 1 time unit to each transition (in ASTRAL null duration transitions are not allowed ). The correctness of the protocol can be formulated into ASTRAL global invariant as follows:

     Forall j:RESP_ID,i:INIT_ID
          ((j.state=commit_final & i=j.source)
                      -> i.Start(Initiate(j))>=0)

which says for any responder, if it committed to an initiator with the identifier stored in the field source, then this initiator really started this instance of the protocol. Our test uncovered the following well-known attack:

1. $A\to I:\{N_a,A\}_{K_i}$

2. $I(A)\to B:\{N_a,A\}_{K_b}$

3. $B\to I(A):\{N_a,N_b\}_{K_a}$

4. $I\to A:\{N_a,N_b\}_{K_a}$

5. $A\to I:\{N_b\}_{K_i}$

6. $I(A)\to B:\{N_b\}_{K_b}$

in 135 seconds, exploring 3657 states with time bound 11 (t starts from 0). The system configuration is 1 initiator , 1 responder and 1 intruder. Note that in fact in our model checker these states are all the legal states traversed by the system instead of the states really checked. As discussed above, at each moment, the model checker will check all possible combinations of calls and transitions, and select only legal transitions to run and discard all the others.

One advantage of ASTRAL is that we can control the behavior of our model checker via the environment (either global or local) clauses, which will significantly reduce the search space of our model checker without rewriting the specification. As in our specification, if we add

         ENVIRONMENT
                Forall i:INIT_ID,j:RESP_INTR_ID
                   (i.Call(Initiate(j),0) & 
                     Forall t:Time (t>0->i.Call(Initiate(j),t)))

which says that any call to the exported transition Initiate that initiates the protocol only happens in time t=0. Our model checker will report the same attack under the same system configuration within 65 seconds with only 587 states explored (time bound still is 11). For larger protocols, we could formulate our preoccupied observation into the environment clause in order to uncover some weakness of the protocol.

TMN Protocol

The TMN protocol is intended to be used in mobile phone systems for session key distribution. It is as follows:

$A\to S: B, \{N_a\}_{K_s}$

$S\to B: A$

$B\to S:A,\{N_b\}_{K_S}$

$S\to A:B, N_b+N_a$

At the end of the protocol, nonce $\{N_b\}$ is taken as a shared secret between initiator A and responder B .

Similar to the case of the Needham-Schroeder protocol, our model is composed of processes representing initiators, responders, servers and the intruder. We also put a counter on each process to indicate the timestamp of the message being sent to the network (the intruder): after each transition's firing, the exit assertion will increase the counter by one so that other processes will know whether this message was already fetched. The correctness of the protocol is formulated as an ASTRAL global invariant:

            Forall j:RESP_ID,i:INIT_ID
              (i.share_secret(j)>0->~Intruder.ifknow_nonce(j))

that is, if an initiator shares a secret with a responder, then the intruder doesn't know the secret.

The intruder can impersonate other legitimate users. Under the simplest setup including 1 initiator, 1 responder, 1 server and the intruder, the model checker finds the following bug:

$A\to S: B, \{N_a\}_{K_s}$

$S\to B: A$

$I(B)\to S:A,\{N_i\}_{K_S}$

$S\to A:B, N_i+N_a$

after searching 3300 states within time bound 8 in 120 seconds. And no other bugs were found with 38,000 states explored in 962 seconds.