--- a/src/HOL/Auth/OtwayRees.thy Thu Oct 09 18:20:14 2003 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Oct 10 11:13:29 2003 +0200
@@ -107,8 +107,6 @@
done
-(**** Inductive proofs about otway ****)
-
(** For reasoning about the encrypted portion of messages **)
lemma OR2_analz_knows_Spy:
@@ -131,10 +129,10 @@
some reason proofs work without them!*)
-(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
+text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
+NOBODY sends messages containing X! *}
-(*Spy never sees a good agent's shared key!*)
+text{*Spy never sees a good agent's shared key!*}
lemma Spy_see_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
by (erule otway.induct, force,
@@ -173,7 +171,7 @@
text{*Session keys are not used to encrypt other session keys*}
-(*The equality makes the induction hypothesis easier to apply*)
+text{*The equality makes the induction hypothesis easier to apply*}
lemma analz_image_freshK [rule_format]:
"evs \<in> otway ==>
\<forall>K KK. KK <= -(range shrK) -->
@@ -185,7 +183,6 @@
apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto)
done
-
lemma analz_insert_freshK:
"[| evs \<in> otway; KAB \<notin> range shrK |] ==>
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
@@ -193,8 +190,7 @@
by (simp only: analz_image_freshK analz_image_freshK_simps)
-(*** The Key K uniquely identifies the Server's message. **)
-
+text{*The Key K uniquely identifies the Server's message. *}
lemma unique_session_keys:
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs;
Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
@@ -202,23 +198,21 @@
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
-(*Remaining cases: OR3 and OR4*)
-apply blast+
+apply blast+ --{*OR3 and OR4*}
done
subsection{*Authenticity properties relating to NA*}
-(*Only OR1 can have caused such a part of a message to appear.*)
+text{*Only OR1 can have caused such a part of a message to appear.*}
lemma Crypt_imp_OR1 [rule_format]:
"[| A \<notin> bad; evs \<in> otway |]
==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|}
\<in> set evs"
-apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
-done
+by (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
lemma Crypt_imp_OR1_Gets:
"[| Gets B {|NA, Agent A, Agent B,
@@ -242,9 +236,9 @@
done
-(*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
+text{*It is impossible to re-use a nonce in both OR1 and OR2. This holds because
OR2 encrypts Nonce NB. It prevents the attack that can occur in the
- over-simplified version of this protocol: see OtwayRees_Bad.*)
+ over-simplified version of this protocol: see OtwayRees_Bad.*}
lemma no_nonce_OR1_OR2:
"[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> otway |]
@@ -254,8 +248,8 @@
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
-(*Crucial property: If the encrypted message appears, and A has used NA
- to start a run, then it originated with the Server!*)
+text{*Crucial property: If the encrypted message appears, and A has used NA
+ to start a run, then it originated with the Server!*}
lemma NA_Crypt_imp_Server_msg [rule_format]:
"[| A \<notin> bad; evs \<in> otway |]
==> Says A B {|NA, Agent A, Agent B,
@@ -267,19 +261,16 @@
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
-(*OR1: it cannot be a new Nonce, contradiction.*)
-apply blast
-(*OR3*)
-apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)
-(*OR4*)
-apply (blast intro!: Crypt_imp_OR1)
+apply blast --{*OR1: by freshness*}
+apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) --{*OR3*}
+apply (blast intro!: Crypt_imp_OR1) --{*OR4*}
done
-(*Corollary: if A receives B's OR4 message and the nonce NA agrees
+text{*Corollary: if A receives B's OR4 message and the nonce NA agrees
then the key really did come from the Server! CANNOT prove this of the
bad form of this protocol, even though we can prove
- Spy_not_see_encrypted_key*)
+ Spy_not_see_encrypted_key*}
lemma A_trusts_OR4:
"[| Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
@@ -293,10 +284,9 @@
by (blast intro!: NA_Crypt_imp_Server_msg)
-(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
+text{*Crucial secrecy property: Spy does not see the keys sent in msg OR3
Does not in itself guarantee security: an attack could violate
- the premises, e.g. by having A=Spy **)
-
+ the premises, e.g. by having @{term "A=Spy"}*}
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
==> Says Server B
@@ -308,9 +298,9 @@
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*)
-(*OR3, OR4, Oops*)
-apply (blast dest: unique_session_keys)+
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
+apply spy_analz --{*Fake*}
+apply (blast dest: unique_session_keys)+ --{*OR3, OR4, Oops*}
done
theorem Spy_not_see_encrypted_key:
@@ -339,8 +329,8 @@
by (blast dest: Spy_not_see_encrypted_key)
-(*A's guarantee. The Oops premise quantifies over NB because A cannot know
- what it is.*)
+text{*A's guarantee. The Oops premise quantifies over NB because A cannot know
+ what it is.*}
lemma A_gets_good_key:
"[| Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
@@ -354,8 +344,8 @@
subsection{*Authenticity properties relating to NB*}
-(*Only OR2 can have caused such a part of a message to appear. We do not
- know anything about X: it does NOT have to have the right form.*)
+text{*Only OR2 can have caused such a part of a message to appear. We do not
+ know anything about X: it does NOT have to have the right form.*}
lemma Crypt_imp_OR2:
"[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> otway |]
@@ -378,12 +368,11 @@
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all)
-(*Fake, OR2*)
-apply blast+
+apply blast+ --{*Fake, OR2*}
done
-(*If the encrypted message appears, and B has used Nonce NB,
- then it originated with the Server! Quite messy proof.*)
+text{*If the encrypted message appears, and B has used Nonce NB,
+ then it originated with the Server! Quite messy proof.*}
lemma NB_Crypt_imp_Server_msg [rule_format]:
"[| B \<notin> bad; evs \<in> otway |]
==> Crypt (shrK B) {|NB, Key K|} \<in> parts (knows Spy evs)
@@ -397,14 +386,11 @@
\<in> set evs)"
apply simp
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
-(*OR1: it cannot be a new Nonce, contradiction.*)
-(*OR2*)
-apply blast
-(*OR3: needs elim: MPair_parts or it takes forever!*)
-apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2)
-(*OR4*)
-apply (blast dest!: Crypt_imp_OR2)
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
+apply blast --{*Fake*}
+apply blast --{*OR2*}
+apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) --{*OR3*}
+apply (blast dest!: Crypt_imp_OR2) --{*OR4*}
done
@@ -424,7 +410,8 @@
by (blast intro!: NB_Crypt_imp_Server_msg)
-(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text B_trusts_OR3} with
+ @{text Spy_not_see_encrypted_key}*}
lemma B_gets_good_key:
"[| Says B Server {|NA, Agent A, Agent B, X',
Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
--- a/src/HOL/Auth/OtwayRees_Bad.thy Thu Oct 09 18:20:14 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Oct 10 11:13:29 2003 +0200
@@ -22,39 +22,39 @@
consts otway :: "event list set"
inductive "otway"
intros
- (*Initial trace is empty*)
- Nil: "[] \<in> otway"
+ Nil: --{*The empty trace*}
+ "[] \<in> otway"
- (*The spy MAY say anything he CAN say. We do not expect him to
- invent new nonces here, but he can also use NS1. Common to
- all similar protocols.*)
- Fake: "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |]
+ Fake: --{*The Spy may say anything he can say. The sender field is correct,
+ but agents don't use that information.*}
+ "[| evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) |]
==> Says Spy B X # evsf \<in> otway"
- (*A message that has been sent can be received by the
- intended recipient.*)
- Reception: "[| evsr \<in> otway; Says A B X \<in>set evsr |]
+
+ Reception: --{*A message that has been sent can be received by the
+ intended recipient.*}
+ "[| evsr \<in> otway; Says A B X \<in>set evsr |]
==> Gets B X # evsr \<in> otway"
- (*Alice initiates a protocol run*)
- OR1: "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
+ OR1: --{*Alice initiates a protocol run*}
+ "[| evs1 \<in> otway; Nonce NA \<notin> used evs1 |]
==> Says A B {|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs1 \<in> otway"
- (*Bob's response to Alice's message.
- This variant of the protocol does NOT encrypt NB.*)
- OR2: "[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
+ OR2: --{*Bob's response to Alice's message.
+ This variant of the protocol does NOT encrypt NB.*}
+ "[| evs2 \<in> otway; Nonce NB \<notin> used evs2;
Gets B {|Nonce NA, Agent A, Agent B, X|} \<in> set evs2 |]
==> Says B Server
{|Nonce NA, Agent A, Agent B, X, Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
# evs2 \<in> otway"
- (*The Server receives Bob's message and checks that the three NAs
+ OR3: --{*The Server receives Bob's message and checks that the three NAs
match. Then he sends a new session key to Bob with a packet for
- forwarding to Alice.*)
- OR3: "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
+ forwarding to Alice.*}
+ "[| evs3 \<in> otway; Key KAB \<notin> used evs3;
Gets Server
{|Nonce NA, Agent A, Agent B,
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|},
@@ -67,10 +67,10 @@
Crypt (shrK B) {|Nonce NB, Key KAB|}|}
# evs3 \<in> otway"
- (*Bob receives the Server's (?) message and compares the Nonces with
- those in the message he previously sent the Server.
- Need B ~= Server because we allow messages to self.*)
- OR4: "[| evs4 \<in> otway; B ~= Server;
+ OR4: --{*Bob receives the Server's (?) message and compares the Nonces with
+ those in the message he previously sent the Server.
+ Need @{term "B \<noteq> Server"} because we allow messages to self.*}
+ "[| evs4 \<in> otway; B \<noteq> Server;
Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
\<in> set evs4;
@@ -78,9 +78,9 @@
\<in> set evs4 |]
==> Says B A {|Nonce NA, X|} # evs4 \<in> otway"
- (*This message models possible leaks of session keys. The nonces
- identify the protocol run.*)
- Oops: "[| evso \<in> otway;
+ Oops: --{*This message models possible leaks of session keys. The nonces
+ identify the protocol run.*}
+ "[| evso \<in> otway;
Says Server B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
\<in> set evso |]
==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> otway"
@@ -91,7 +91,7 @@
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
-(*A "possibility property": there are traces that reach the end*)
+text{*A "possibility property": there are traces that reach the end*}
lemma "[| B \<noteq> Server; Key K \<notin> used [] |]
==> \<exists>NA. \<exists>evs \<in> otway.
Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
@@ -111,10 +111,7 @@
done
-(**** Inductive proofs about otway ****)
-
-
-(** For reasoning about the encrypted portion of messages **)
+subsection{*For reasoning about the encrypted portion of messages *}
lemma OR2_analz_knows_Spy:
"[| Gets B {|N, Agent A, Agent B, X|} \<in> set evs; evs \<in> otway |]
@@ -131,20 +128,20 @@
==> K \<in> parts (knows Spy evs)"
by blast
-(*Forwarding lemma: see comments in OtwayRees.thy*)
+text{*Forwarding lemma: see comments in OtwayRees.thy*}
lemmas OR2_parts_knows_Spy =
OR2_analz_knows_Spy [THEN analz_into_parts, standard]
-(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
- sends messages containing X! **)
+text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
+NOBODY sends messages containing X! *}
-(*Spy never sees a good agent's shared key!*)
+text{*Spy never sees a good agent's shared key!*}
lemma Spy_see_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
-apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
-done
+by (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
+
lemma Spy_analz_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
@@ -155,10 +152,10 @@
by (blast dest: Spy_see_shrK)
-(*** Proofs involving analz ***)
+subsection{*Proofs involving analz *}
-(*Describes the form of K and NA when the Server sends this message. Also
- for Oops case.*)
+text{*Describes the form of K and NA when the Server sends this message. Also
+ for Oops case.*}
lemma Says_Server_message_form:
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
evs \<in> otway |]
@@ -178,9 +175,9 @@
****)
-(** Session keys are not used to encrypt other session keys **)
+text{*Session keys are not used to encrypt other session keys*}
-(*The equality makes the induction hypothesis easier to apply*)
+text{*The equality makes the induction hypothesis easier to apply*}
lemma analz_image_freshK [rule_format]:
"evs \<in> otway ==>
\<forall>K KK. KK <= -(range shrK) -->
@@ -199,8 +196,7 @@
by (simp only: analz_image_freshK analz_image_freshK_simps)
-(*** The Key K uniquely identifies the Server's message. **)
-
+text{*The Key K uniquely identifies the Server's message. *}
lemma unique_session_keys:
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} \<in> set evs;
Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} \<in> set evs;
@@ -208,14 +204,13 @@
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
-(*Remaining cases: OR3 and OR4*)
-apply blast+
+apply blast+ --{*OR3 and OR4*}
done
-(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
+subsection{*Crucial secrecy property: Spy does not see the keys sent in msg OR3
Does not in itself guarantee security: an attack could violate
- the premises, e.g. by having A=Spy **)
+ the premises, e.g. by having @{term "A=Spy"} *}
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> otway |]
@@ -228,9 +223,9 @@
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*)
-(*OR3, OR4, Oops*)
-apply (blast dest: unique_session_keys)+
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
+apply spy_analz --{*Fake*}
+apply (blast dest: unique_session_keys)+ --{*OR3, OR4, Oops*}
done
@@ -244,26 +239,25 @@
by (blast dest: Says_Server_message_form secrecy_lemma)
-(*** Attempting to prove stronger properties ***)
+subsection{*Attempting to prove stronger properties *}
-(*Only OR1 can have caused such a part of a message to appear.
- The premise A \<noteq> B prevents OR2's similar-looking cryptogram from being
- picked up. Original Otway-Rees doesn't need it.*)
+text{*Only OR1 can have caused such a part of a message to appear. The premise
+ @{term "A \<noteq> B"} prevents OR2's similar-looking cryptogram from being picked
+ up. Original Otway-Rees doesn't need it.*}
lemma Crypt_imp_OR1 [rule_format]:
"[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) -->
Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs"
-apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
-done
+by (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
-(*Crucial property: If the encrypted message appears, and A has used NA
+text{*Crucial property: If the encrypted message appears, and A has used NA
to start a run, then it originated with the Server!
- The premise A \<noteq> B allows use of Crypt_imp_OR1*)
-(*Only it is FALSE. Somebody could make a fake message to Server
- substituting some other nonce NA' for NB.*)
+ The premise @{term "A \<noteq> B"} allows use of @{text Crypt_imp_OR1}*}
+text{*Only it is FALSE. Somebody could make a fake message to Server
+ substituting some other nonce NA' for NB.*}
lemma "[| A \<notin> bad; A \<noteq> B; evs \<in> otway |]
==> Crypt (shrK A) {|NA, Key K|} \<in> parts (knows Spy evs) -->
Says A B {|NA, Agent A, Agent B,
@@ -275,15 +269,12 @@
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
apply (erule otway.induct, force,
drule_tac [4] OR2_parts_knows_Spy, simp_all)
-(*Fake*)
-apply blast
-(*OR1: it cannot be a new Nonce, contradiction.*)
-apply blast
-(*OR3 and OR4*)
+apply blast --{*Fake*}
+apply blast --{*OR1: it cannot be a new Nonce, contradiction.*}
+txt{*OR3 and OR4*}
apply (simp_all add: ex_disj_distrib)
-(*OR4*)
-prefer 2 apply (blast intro!: Crypt_imp_OR1)
-(*OR3*)
+ prefer 2 apply (blast intro!: Crypt_imp_OR1) --{*OR4*}
+txt{*OR3*}
apply clarify
(*The hypotheses at this point suggest an attack in which nonce NB is used
in two different roles: