Coursework for ECMM462 Fundamentals of Security Module Convener: Diego Marmsoler Submission date: Wednesday, November 11th, 2020 For your continuous assessment you will analyse a protocol for security weak- nesses. The assessment contain three types of tasks and you can get up to 100 marks in total: Informal (marked as I): up to 40 marks Specification (marked as S): up to 40 marks Verification (marked as V ): up to 20 marks For the specification and verification tasks you will need to use the proof assistant Isabelle which can be downloaded from http://isabelle.in.tum.de/. The assessment is worth 30% of the overall module mark. You need to submit a PDF with your answers and any Isabelle theories via the electronic submission system E-BART (https://bart.exeter.ac.uk/). 1 A Simple Protocol to Exchange a Secret Nonce The Message Sequence Chart depicted in Fig. 1 describes a simple protocol for the exchange of a secret nonce N between two agents A and B The initial knowledge of agent A and agent B is given in set notation and shown in the corresponding boxes: Agent A knows her own public and private keys PUA and PRA as well as agent B’s public key PUB. Agent B knows his own public and private keys PUB and PRB as well as agent A’s public key PUA. Agent A initiates the protocol by sending a message containing her identity IDA to agent B (1). Upon reception of the message, agent B generates a new random nonce N and encrypts N with agent A’s public key. Finally, agent B creates a new message which contains the encrypted nonce E(PUA, N) and sends it back to agent A (2). Agent A {PUA,PRA,PUB} Agent B {PUB,PRB,PUA} (1) IDA (2) E(PUA, N) Figure 1: Simple protocol to exchange a secret nonce. 2 1. Create a Model of the Protocol 10 marks Your first task is to model the protocol in Isabelle: First, create a new theory Exchange.thy which imports theory Event.thy discussed in the lecture (S: 2 marks). Then, define a set exchange::event list set, which contains all event se- quences satisfying the protocol specification from Fig. 1 (S: 8 marks). Note that the nonce created by agent B needs to be a fresh one, i.e. one which was not used so far. 2. Describe a Valid Execution Trace 10 marks Your next task is to describe an execution which contains at least two events and satisfies the protocol: First, describe the sequence of events informally using a Message Sequence Chart (I: 5 marks). Next, define the execution in Isabelle as a list of events1 (S: 3 marks). Finally, verify in Isabelle that the defined execution is indeed an element of the set exchange (V: 2 marks). Hint: For the last question you may need the lemma used.used Cons from the- ory Event.thy and the lemmas generated by Isabelle from the definition of set exchange. 3. Describe an Impossible Execution Trace 10 marks For this task you need to describe an execution which contains at least two events and violates the protocol: First, describe the sequence of events informally using a Message Sequence Chart and explain where it violates the protocol specification (I: 5 marks). Next, define the execution in Isabelle as a list of events (S: 3 marks). Finally, verify in Isabelle that the defined execution is indeed not an element of the set exchange (V: 2 marks). Hint: For the last question you may need to use the proof method rule notI and derive a contradiction from the assumption that the execution is an element of the set exchange. 1For the definition of example executions you can also abbreviations instead of a definitions. 3 4. Describe a Potential Attack Trace 10 marks Assuming there is a passive spy who can intercept and read all messages sent between agents but which cannot modify messages. This task requires you to show that the spy can obtain the encrypted2 nonce. To this end you need to describe a possible execution in which the spy learns a message containing the encrypted nonce: First, describe the sequence of events informally using a Message Sequence Chart and explain how the knowledge of the spy changes with every event (I: 5 marks). Then, define the execution in Isabelle as a list of events and verify in Isabelle that the spy can learn the encrypted message from this execution, i.e. that the spy can analyse it from the knowledge he/she acquires during the execution (S+V: 5 marks). 5. Show that the Attack is not Successful 10 marks For this task you need to verify that the spy cannot learn the nonce from the execution developed for the previous task: First, refer to the Message Sequence Chart developed for the task described in Sect.4, to explain informally why the spy cannot learn the nonce (I: 5 marks). Then, verify in Isabelle that the spy cannot learn the message from the exe- cution defined in Isabelle for the task described in Sect. 4 (S+V: 5 marks). 6. Show that the Protocol is Secure 15 marks This task requires you to verify that the protocol is secure against eavesdropping: First, explain informally how the protocol ensures that the spy can never obtain nonce N (I: 5 marks). Then, specify this security requirement as a theorem in Isabelle (S: 5 marks). Finally, verify the requirement in Isabelle by proving the theorem (V: 5 marks). Hint: The proof is done using rule induction ((induction rule: exchange.induct)). Moreover you may need to use lemma prikey provided in Appendix A. 2Note that the spy only needs to learn the encrypted message containing the nonce and not the nonce itself. 4 7. Make the Spy Stronger 10 marks Assume now that the spy can not only intercept and read messages but also modify them. For this task you need to adapt the specification of set exchange to include possible modifications to messages from the spy (S: 10 marks). 8. Show that the Protocol is not Secure 10 marks Your next task requires you to show that the protocol is not secure against a spy as described in Sect. 7: First, use a Message Sequence Chart to informally describe a possible sequence of events in which the spy obtains the nonce (I: 5 marks). Then, define the execution in Isabelle as a list of events and verify in Is- abelle that the spy can learn the nonce from this execution, i.e. that the spy can analyse it from the knowledge he/she acquires during the execution (S+V: 5 marks). 9. Fix the Protocol 15 marks Your last task requires you to propose a possible solution for the problem described in Sect. 8: First, describe informally how the protocol could be changed to cope with a spy as introduced in Sect. 7 (I: 10 marks). Then, implement the change in Isabelle, adapting the specification of set exchange (S: 2 marks). Finally, verify that the spy cannot learn the nonce from the execution devel- oped for the previous task (Sect. 8) any more, i.e. that the spy cannot analyse it from the knowledge he/she acquires during the execution (V: 3 marks). 5 A. Appendix lemma pr ikey : assumes ”A 6= Spy” shows ” evs ∈ exchange =⇒ Key ( priK A) /∈ ana lz ( knows Spy evs )” proof ( induct i on r u l e : exchange . induct ) case Ni l then show ?case using assms by simp next case (RQ evs1 A B) then show ?case by simp next case (RS evs2 N B A) then show ?case by simp qed 6
欢迎咨询51作业君