Reference no: EM133214258

Consider the following four-step communication protocol, which is known as Kerberos protocol and its aim is to guarantee authentication and key exchange between a client and a server [1, 2].

(1) A -> S : A, B

(2) S -> A : {Ts, L, Kab, B}Kas , {Ts, L, Kab, A}Kbs (3) A -> B : {Ts, L, Kab, A}Kbs , {A, Ta} Kab

(4) B -> A : {Ta+1}Kab

The protocol involves the principals A (client/initiator) and B (server/responder), and an authentication server S. The server S is a trusted party which shares a key Kas with A and a key Kbs with B, and also responsible for generating new session keys Kab. The above protocol makes use of the time stamps Ta and Tb, and the lifetime L. In step (1) above, A contacts S in order to communicate its claimed identity and the name of the server B. In step (2), S sends to A two encrypted components. The first component contains the session key Kab generated by S, a time stamp Ts specifying when the session key has been generated, the interval of validity of such key, and the name of the server B. The second component is called ticket having similar information, however, A will not be able to decrypt it. In step (3), A forwards the ticket to server B, with a authenticator component encrypted with the new session key. After receiving the above message, B can extract the session key from the ticket, and uses it to decrypt the authenticator. If the key used to encrypt authenticator matches with the key contained in the ticket, the server B can assume that the authenticator was generated by A. At this point, in order to authenticate the client A, the server B must also check the time stamp Ta to make sure that the authenticator is recent. Thus B can recognise A if the result of verification is positive. In step (4), B demonstrate its identity to A sending a message with increased time stamp encrypted with the session key Kab.

The model of the above protocol could be composed of several variables and processes (or agents). The protocol shall ensure authentication and secrecy. Such properties shall be verified against an intruder I with the following capabilities:

• I is a known agent, it can act either as initiator or as responder of a protocol session;
• I can eavesdrop and store any message sent by any agent;
• I can exploit its knowledge to generate new messages or use previously storedmessages as they are.

Model as a concurrent system in NuSMV the protocol described above as the interaction of 4 agents, A, B, S and I. Multiple sessions may overlap, asynchronously. However, to ensure finiteness of the model state space, consider a maximum number n of sessions, and verify the satisfaction of the properties above under such a limitation. To model and verify the desired system properties you need to complete the following tasks:

Task 1: Design and draw a state transition diagram of the system considering four agents mentioned above. Please note that this diagram would be a high-level diagram and not considering NuSMV's low level diagram (as it would be very complicated);

Task 2: In your NuSMV model (code using the SMV language) all the agents should work concurrently, and in an asynchronous manner;

Task 3: Identify and express six authentication and secrecy properties using CTL/LTL;