Learning outcome 1: Demonstrate the application of formalisms to specify system properties using CSP

Learning outcome 2: Use tools and analysis techniques to study and reason about critical properties of the concurrent systems, including security protocols

The learning objective of this coursework is to design, analyse, and verify a concurrent system using the CSP/FDR model checker, and use Casper to verify security protocols. This will give you hands-on experience with CSP/FDR/Casper 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. 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.

Section 2: Task Specification

Task 1: CSP and the concurrent systems
A bridge over a river is only wide enough to permit a single lane of traffic. Therefore, cans can only move concurrently if they are moving in the same direction. For the simplicity of modelling, we consider all the cars moving from left to right are RED, and all from right to left are BLUE. For example, some blue cars entering the bridge are illustrated by the following diagram.
However, a crash can occur if two cars moving in different directions enter the bridge at the same time, which violates the safety property.

A car can approach the bridge, enter and leave the bridge. Note that we don't consider any time issue in the system. For example, cars enter or leave the bridge instantaneously. In the system, there are THREE red cars and THREE blue cars, which can move concurrently.

To model the system, THREE processes should be constructed at least, i.e., one process to denote the concurrent behaviour of three red cars, and one for three blue cars, and one to model the bridge to interactive with all cars.

Task 1.1: Design and draw a labelled transition diagram of the bridge. The bridge should be able to interact with any car. However, it must follow one rule that the car enters the bridge firstly and leaves the bridge firstly. The one lane system does not allow the overtaking. The system can identify some ‘bad' behaviours which violate the safety property and can lead to the event ‘crash'.

Note that the event crash should not interfere the behaviour of the bridge. For example, the occurrence of the event crash should not stop the system. Overall, the transition system of the bridge should satisfy three requirements:
• Identification of the ‘bad' behaviours to violate the safety property (no crash);
• Controlling of the cars with the first-in and first-out rule;
• No interference on cars' behaviours except that it satisfies the above requirements.

Task 1.2: Construct the complete system (cars and the bridge) and verify the safety property to check whether the event crash can happen. The CSP scripts for the system and the specification should be given in FDR, in which the refinement should be executed too.

Task 1.3 To satisfy the safety property that no crash can happen, we introduce two signals, which are modelled as two events, to design a control system. When a car approaches the bridge, it must obtain the near-end signal first, and then obtain the far-end signal to lock the bridge. That is, a car must obtain two signals to enter the bridge. When the car has entered the bridge, it releases the near-end signal so that the latter car can obtain it. When the car leaves the bridge, it releases the far-end signal.

You need to redesign the processes for the cars and the bridge to allow the signal events, and use the refinement to prove the safety property. The new system with the signals should be given in FDR with the related safety property refinement.

Task 1.4: Verify the system with the signals from Task 3 is deadlocked free. If you can find the deadlock in the system from the model checking, you can redesign the behaviour of a car or introduce another controller or mechanism to avoid the deadlock.

Model your modification in FDR with the refinement. Note that the modified system must hold all the properties from the previous task. Three jobs should be done:
• The refinement of deadlock freedom for the system
• The modification of related processes to avoid deadlock
• The new refinement of the modified system to prove it's deadlock free

Task 1.5: We extend the system by adding more cars here, and we assume there are SIX red cars and SIX blue cars. One potential problem for the design in Task 4 is that a certain group of cars may get an advantage than another group to obtain the signals. Therefore, you need to design a fairer controller which allows three cars with the same colour maximally to go through the bridge, and then pass the signals to the cars with another colour.

Model such a controller in FDR, and verify it by showing the traces with more than three cars in the same direction is not allowed.

Task 1.6: Produce a mini report to explain and discuss your design or any issue from Task 1.1 to Task 1.5. For example, you may explain some tricky parts of the CSP scripts to enable the reader to understand why this design satisfies the requirements of the tasks.
This report should be 800 words maximum

Task 2: Casper for Security Protocols

Consider the following four-step communication protocol, which is a simplified version of a well- known 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: Model the security protocol's authentication and secrecy in Casper. You should produce a Casper file (*.sql), convert it into a FDR script in Casper and finally model check the two properties in FDR.

Task 2.2: 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

Section 3: Deliverables

One folder in zip format (only) must be uploaded via the relevant link on the module's space on Blackboard. The zipped file should be named as ‘AVCS_Your Name_Student Number.zip'.

The link will be available two weeks before the due date and will be communicated to students via an email announcement.

You can produce ONE FDR script for Task 1.2 to Task 1.5, or produce a FDR script for each task, up to your own convenience. For the transition diagram in Task 1.1, you can draw it in Word or any software, or you can draw it by hand and insert it as a picture took by your mobile phone.

The folder must contain:
• One FDR or multiple FDR scripts for Task 1.2 to Task 1.5
• A word / PDF file for Task 1.1 and Task 1.6
• One Casper file (*.sql) for Task 2.1
• One FDR script generated by Casper from Task 2.1
• A word / PDF file for Task 2.2

Section 4: Academic Offences

This is an individual coursework, therefore you should individually submit your own original work. In fact, we encourage you to work as a group or cohort. You are free to discuss the solutions for the coursework, however, you should then split up and work alone to finish the work. The identical work is definitely an offence, and the similar work with effortless changes (such as the change of event names) is considered an offence too.

Please do not share your work with any one. Even if you don't share your code on purpose, you are still considered a collusion if the similar work is found. For example, your friend may request your work for a reference, and promise not to copy your code. However, very often they may take the risk when the deadline is approaching. For this case, all the involved students may get the same penalty.

The teaching team is professional about programming and marking. You might be invited for an interview to demonstrate and explain your program if the markers and the module leader doubt the originality of your work.

Section 5: Marking Criteria

The following table (please see next page) gives details of the marking criteria for this coursework. Marks will be awarded for clear rationale justifying design choices.

The reports for Task 1.6 and Task 2.2 can help the markers to map the full logic of the solution into the correct marking section.

Code should be well structured, appropriately commented, neat and efficient.

The marking band is incremental. For example, the claim of 70-85 means your work has satisfied any precedent band.

Section 6: Feedback mechanisms

Formative / Verbal will be provided during practical sessions.

Written feedback will be provided on blackboard along with the marked for the submitted work on 13 February 2023.

Attachment:- Analysis and Verification of Concurrent Systems.rar