” ECMM462程序 写作、 写作Python，Java语言编程Coursework for ECMM462Submission date: Wednesday, November 11th, 2020For your continuous assessment you will analyse a protocol for security weaknesses.The assessment contain three types of tasks and you can get up to 100marks in total:Informal (marked as I): up to 40 marksSpecification (marked as S): up to 40 marksVerification (marked as V ): up to 20 marksFor the specification and verification tasks you will need to use the proof assistantIsabelle which can be Downloaded from https://isabelle.in.tum.de/.The assessment is worth 30% of the overall module mark. You need to submita PDF with your answers and any Isabelle theories via the electronic submissionsystem E-BART ( httpss://bart.exeter.ac.uk/).1A Simple Protocol to Exchange a Secret NonceThe Message Sequence Chart depicted in Fig. 1 describes a simple protocol for theexchange of a secret nonce N between two agents A and B The initial knowledgeof agent A and agent B is given in set notation and shown in the correspondingboxes:Agent A knows her own public and private keys PU A and PRA as well as agent Bspublic key PU B.Agent B knows his own public and private keys PU B and PRB as well as agent Aspublic key PU A.Agent A initiates the Protocol by sending a message containing her identity IDAto agent B (1). Upon reception of the message, agent B generates a new randomnonce N and encrypts N with agent As public key. Finally, agent B creates anew message which Contains the encrypted nonce E(PU A, N) and sends it back toagent A (2).Agent A {PU A,PRA,PU B} Agent B {PU B,PRB,PU A}(1) IDA(2) E(PU A, N)Figure 1: Simple protocol to exchange a secret nonce.21. Create a Model of the Protocol10 marksYour first task is to model the protocol in Isabelle:First, create a new theory Exchange.thy which imports theory Event.thydiscussed in the lecture (S: 2 marks).Then, define a set exchange::event list set, which contains all event sequencessatisfying 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 wasnot used so far.2. Describe a Valid Execution Trace10 marksYour next task is to describe an execution which contains at least two events andsatisfies the protocol:First, describe the Sequence of events informally using a Message SequenceChart (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 ofthe set exchange (V: 2 marks).Hint: For the last question you may need the lemma used.used Cons from theoryEvent.thy and the lemmas generated by Isabelle from the definition of setexchange.3. Describe an Impossible Execution Trace10 marksFor this task you need to describe an execution which contains at least two eventsand violates the protocol:First, describe the sequence of events informally using a Message SequenceChart 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 elementof the set exchange (V: 2 marks).Hint: For the last question you may need to use the proof method rule notI andderive a contradiction From the assumption that the execution is an element of theset exchange.1For the definition of example executions you can also abbreviations instead of a definitions.34. Describe a Potential Attack Trace10 marksAssuming there is a passive spy who can intercept and read all messages sentbetween agents but which cannot modify messages.This task requires you to show that the spy can obtain the encrypted 2 nonce.To this end you need to describe a possible execution in which the spy learns amessage containing the encrypted nonce:First, describe the sequence of events informally using a Message SequenceChart 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 Isabellethat the spy can learn the encrypted message from this execution, i.e. that thespy can analyse it from the knowledge he/she acquires during the execution(S+V: 5 marks).5. Show that the Attack is not Successful10 marksFor this task you need to verify that the spy cannot learn the nonce from theexecution developed for the previous task:First, refer to the Message Sequence Chart developed for the task described inSect.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 executiondefined in Isabelle For the task described in Sect. 4 (S+V: 5 marks).6. Show that the Protocol is Secure15 marksThis task requires you to verify that the protocol is secure against eavesdropping:First, explain informally how the protocol ensures that the spy can neverobtain 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 thenonce itself.47. Make the Spy Stronger10 marksAssume now that the spy can not only intercept and read messages but also modifythem. For this task you need to adapt the specification of set exchange to includepossible Modifications to messages from the spy (S: 10 marks).8. Show that the Protocol is not Secure10 marksYour next task requires you to show that the protocol is not secure against a spyas described in Sect. 7:First, use a Message Sequence Chart to informally describe a possible sequenceof 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 Isabellethat the spy can learn the nonce from this execution, i.e. that thespy can analyse it from the knowledge he/she acquires during the execution(S+V: 5 marks).9. Fix the Protocol15 marksYour last task requires you to propose a possible solution for the problem describedin Sect. 8:First, describe informally how the protocol could be changed to cope with aspy as introduced in Sect. 7 (I: 10 marks).Then, implement the Change in Isabelle, adapting the specification of setexchange (S: 2 marks).Finally, verify that the spy cannot learn the nonce from the execution developedfor the previous task (Sect. 8) any more, i.e. that the spy cannot analyseit from the Knowledge he/she acquires during the execution (V: 3 marks).5A. Appendixlemma p ri k e y :assumes A 6= Spyshows e v s exchange = Key ( priK A) / a n al z ( knows Spy e v s ) proof ( i n d u c ti o n r u l e : exchange . i n d u c t )case Nilthen show ?case Using assms by simpnextcase (RQ e v s 1 A B)then show ?case by simpnextcase (RS e v s 2 N B A)then show ?case by simpqed如有需要，请加QQ：99515681 或邮箱：99515681@qq.com
“
添加老师微信回复‘’官网 辅导‘’获取专业老师帮助，或点击联系老师1对1在线指导。
