next up previous
Next: CSP Description Up: CSP, PVS and a Previous: Traces

The protocol

In [BO97] an authentication protocol is proposed, which is further explained in [Pau97]. This protocol operates over an arbitrarily long chain of protocol agents, terminating with a key-server. We set out to verify that a run of the protocol establishes an uncompromised chain of session keys between adjacent pairs of agents. The protocol operates as follows, where $\mathsf{Hash}X$ is the hash of a message X and $\mathsf{Mac}_K X$ is the pair $\{\mathsf{Hash}\{K, X\}, X\}$. In the protocol description, K will be an agent's long-term shared key, and the hashed message $\mathsf{Hash}\{K, X\}$ ( a message authentication code) will allow the server to check that message X originated with the owner of key K . $K_x$ is the long-term key of agent X , $K_{xy}$ is a session key between agent X and agent Y , $N_x$ is a fresh nonce and $\mathsf{null}$ is a placeholder.

Agent A initiates a run by sending the following message.

1.~A \rightarrow B : \mathsf{Mac}_{K_a}\{A,B,N_a,\mathsf{null}\}\end{displaymath}

Agent B responds by sending a similar message to agent C , but replacing the placeholder with A 's entire message.

2.~B \rightarrow C : \mathsf{Mac}_{K_b}\{B,C,N_b,\mathsf{Mac}_{K_a}\{A,B,N_a,\mathsf{null}\}\}\end{displaymath}

This step is repeated for each subsequent agent in the chain, and each agent adds new components to the message, and passes it on. This stage terminates when some agent specifies the server as the recipient. Suppose, for example, that C sends the message to the server.

3.~ C \rightarrow S : \mathsf{Mac}_{K_c}\{C,S,N_c,\mathsf{Mac}_{K_b}\{B,C,N_b,\mathsf{Mac}_{K_a}\{A,B,N_a,\mathsf{null}\}\}\}\end{displaymath}

The server now unpacks this message, and prepares session keys for each adjacent pair of agents in the chain. Considering the outer two levels of the protocol, we can see that agent C was called by agent B , and called agent S (the server). The server therefore generates the session keys $K_{bc}$ and $K_{cs}$, prepares two certificates, and encrypts them with agent C 's secret key: $\{K_{cs},S,N_c\}_{K_c}$ and $\{K_{bc},B,N_c\}_{K_c}$. In a sense, the key $K_{cs}$ is redundant, because agent C has a key with the server already -- its longterm key $K_c$. However, including it allows the final agent in the chain to be treated like any other agent.

Ignoring the first level of the message now, and considering the second and third levels, the server creates two certificates for agent B : $\{K_{bc},C,N_b\}_{K_b}$ and $\{K_{ab},A,N_b\}_{K_b}$,encrypted with agent B 's secret key.

The third level of the message contains the placeholder $\mathsf{null}$, which indicates to the server that this is the last level of the message. It therefore prepares only one further certificate: $\{K_{ab},B,N_a\}_{K_a}$.

In the next step, the server returns the all certificates to the last agent on the chain:

4.~S \rightarrow C: 
 ...b}, \ \{K_{ab},A,N_b\}_{K_b}, \{K_{ab},B,N_a\}_{K_a}\end{drop}\end{displaymath}

Agent C removes the relevant certificates and forwards the rest to agent B, which in turn passes the final one on to agent A.

5.~C \rightarrow B : \{K_{bc},C,N_b\}_{K_b...
 ...K_a} \ 6.~B \rightarrow A : \{K_{ab},B,N_a\}_{K_a} \end{array}\end{displaymath}

next up previous
Next: CSP Description Up: CSP, PVS and a Previous: Traces