讲解留学生Processing|辅导Web开发|解析Java程序|辅导Web开发
- 首页 >> Python编程 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
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