ECMM462程序代做、代做Python，Java语言编程、c++代写编程代做

日期：2020-11-16 11:12

Coursework for ECMM462

Submission date: Wednesday, November 11th, 2020

For your continuous assessment you will analyse a protocol for security weaknesses.

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 PU A and PRA as well as agent B’s

public key PU B.

Agent B knows his own public and private keys PU B and PRB as well as agent A’s

public key PU A.

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(PU A, N) and sends it back to

agent 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.

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 sequences

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 theory

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 encrypted 2 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 execution

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 Isabelle

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 developed

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 p ri k e y :

assumes ”A 6= Spy”

shows ” 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 Nil

then show ?case using assms by simp

next

case (RQ e v s 1 A B)

then show ?case by simp

next

case (RS e v s 2 N B A)

then show ?case by simp

qed

6