UFCFYN15M Analysis and Verification of Concurrent System

This assignment assesses the following module learning outcomes:

The assignment Is worth 100 marks representing 40% of the overall mark for the module.

The learning objective of this coursework is to design, analyse, and verify authentication protocol using the NuSMV model checker. This will give you hands-on experience with the NuSMV tool and understanding its input language for specifying systems and desired system properties.

The assignment is described in more detail in Section 2.

Assignment type: this is an individual assignment. Do not copy and paste work from any other source or work with any other person. You are strictly forbidden from discussing your answers with another student. Text-matching software will be used on all submissions.

Working on this assignment will help you to achieve the learning outcomes mentioned above as well as you would be aware of when and how you might deploy formal verification techniques. If you have questions about this assignment, I will be happy to discuss those during our lecture/lab session.

Consider the following five-step communication protocol with symmetric key, which is known as Needham-Schroeder protocol used to secure an insecure network. The protocol involves the principals A (initiator) and B (responder), and an authentication server S.

Step 1: Machine A sends a message to Server S, intending to communicate with Machine B, where NA is a Nonce generated by Machine A.

A -> S : A, B, NA

Step 2: Server S sends message back to the Machine A containing KAB, and one more encrypted copy of KAB which will be send to the Machine B by the Machine A. KA and K8 are the Keys of A and B shared with S, respectively. Kee is a secret session key for A and B provided by S.

S -> A : (NA, B, KAB, {KAB,A}K8) KA

Step 3: Machine A forwards {KAB, A}K8, encrypted copy of KAB from Step 2, to the Machine B. With the key it has, Machine B can decrypt it. This is because the message has been encrypted by S with the symmetric key KB of the Machine B.

A -> B: (KAB,A}K8

Step 4: Machine B replies to the Machine A by sending a nonce value encrypted by KAB, confirming that machine B has the secret session key provided by the server S.

B -> A : {NB}KAB

Step 5: Machine A then performs a simple operation on the machine B's nonce.

A -> B : {NB-I}Ko

There is still some vulnerability in this protocol for replay attacks. The model of the above protocol could be composed of several variables and processes. The protocol shall ensure authentication and secrecy. Such properties shall be verified in the presence of adversary I who can

(1) Intercept messages;

(2) Delay messages;

(3) Read and copy messages; and

(4) Generate messages. However, who does not know secret keys of principals, which they share with the authentication server.

(5) Model as a concurrent system in NuSMV the protocol described above as the interaction of processes, 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.

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 processes A, B, S and I mentioned above. Note that this should be a high-level transition system just showing the interaction of the processes and not the NuSMV transition (which will be very complex, and you may not be able to draw it).

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

Task 3: Identify and express at least four authentication and secrecy properties using either in CTL or LTL.

Task 4: Run your code to verify all of the properties identified above. For each property, analyse the verification result to see whether it explains why a property in your model is true or false, and if the result is what you expected. Please note that you don't have to show any simulation results using the "simulate -i -k" command.

Task 5: Q/A session during the demo.

 Section 3: Deliverables

(i) system design and state transition diagram,

(ii) the verification results showing the execution logs. The logs should clearly show verified properties as "true" or "false". In case of "false" it must show a counter example, and

(iii) self-assessment completed form.