Task 2: Casper for Security Protocols (30%) Consider the following four-step communication protocol, which is a simplified version of a wellknown security protocol, and its aim is to guarantee authentication and key exchange between a client and a server. (1) A -> S : A, B (2.1) S -> A : {Ts, Kab, B}Kas (2.2) S -> A : {Ts, Kab, A}Kbs (3.1) A -> B : {Ts, Kab, A}Kbs (3.2) A -> B : {A, Ta} Kab (4) B -> A : {Ta}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 responsible for generating new session keys Kab. The above protocol makes use of the time stamps Ta and Tb. 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 an 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 Ta 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 J with the following capabilities:

J is a known agent, it can act either as initiator or as responder of a protocol session;

J can eavesdrop and store any message sent by any agent;

J can exploit its knowledge to generate new messages or use previously stored messages as they are

Task 2.1: (25%) Model the security protocols authentication and secrecy in Casper. You should produce a Casper file (*.spl), convert it into a FDR script in Casper and finally model check the two properties in FDR.

Task 2.2: (5%) Produce a mini report to analyse the result from FDR. For example, if FDR can find an attack, you should simply talk about how the attack can be implemented. If no attack is found, you should conclude that the protocol holds the properties. The report should be 500 words maximum