Conversion of all main protocols from "Shared" to "Public".
Removal of Key_supply_ax: modifications to possibility theorems.
Improved presentation.
--- a/src/HOL/Auth/CertifiedEmail.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Fri Sep 26 10:34:28 2003 +0200
@@ -156,7 +156,7 @@
apply (erule rev_mp)
apply (erule certified_mail.induct, simp_all)
txt{*Fake*}
-apply (blast dest: Fake_parts_insert_in_Un);
+apply (blast dest: Fake_parts_insert_in_Un)
txt{*Message 1*}
apply blast
txt{*Message 3*}
@@ -170,7 +170,7 @@
lemma Spy_know_private_keys_iff [simp]:
"evs \<in> certified_mail
==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
-by (blast intro: elim:);
+by blast
lemma Spy_dont_know_TTPKey_parts [simp]:
"evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)"
@@ -210,7 +210,7 @@
"evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
apply (erule certified_mail.induct, simp_all)
txt{*Fake*}
-apply (blast dest: Fake_parts_insert_in_Un);
+apply (blast dest: Fake_parts_insert_in_Un)
txt{*Message 1*}
apply blast
txt{*Message 3*}
@@ -246,8 +246,7 @@
apply (frule_tac hr_form, assumption)
apply (elim disjE exE)
apply (simp_all add: parts_insert2 parts_insert_knows_A)
- apply (blast dest!: Fake_parts_sing_imp_Un)
-apply (blast intro: elim:);
+ apply (blast dest!: Fake_parts_sing_imp_Un, blast)
done
@@ -333,7 +332,7 @@
text{*Nobody can have used non-existent keys!*}
-lemma new_keys_not_used [rule_format, simp]:
+lemma new_keys_not_used [simp]:
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> certified_mail|]
==> K \<notin> keysFor (parts (spies evs))"
apply (erule rev_mp)
--- a/src/HOL/Auth/KerberosIV.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,11 +2,11 @@
ID: $Id$
Author: Giampaolo Bella, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-
-The Kerberos protocol, version IV.
*)
-theory KerberosIV = Shared:
+header{*The Kerberos Protocol, Version IV*}
+
+theory KerberosIV = Public:
syntax
Kas :: agent
@@ -128,7 +128,7 @@
(*---------------------------------------------------------------------*)
(*FROM Kas *)
- K2: "[| evs2 \<in> kerberos; Key AuthKey \<notin> used evs2;
+ K2: "[| evs2 \<in> kerberos; Key AuthKey \<notin> used evs2; AuthKey \<in> symKeys;
Says A' Kas {|Agent A, Agent Tgs, Number Ta|} \<in> set evs2 |]
==> Says Kas A
(Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2),
@@ -163,7 +163,8 @@
specification. Adding it strengthens the guarantees assessed by the
protocol. Theorems that exploit it have the suffix `_refined'
*)
- K4: "[| evs4 \<in> kerberos; Key ServKey \<notin> used evs4; B \<noteq> Tgs;
+ K4: "[| evs4 \<in> kerberos; Key ServKey \<notin> used evs4; ServKey \<in> symKeys;
+ B \<noteq> Tgs; AuthKey \<in> symKeys;
Says A' Tgs {|
(Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
Number Tk|}),
@@ -189,9 +190,9 @@
(*---------------------------------------------------------------------*)
(* FROM the initiator *)
- K5: "[| evs5 \<in> kerberos;
+ K5: "[| evs5 \<in> kerberos; AuthKey \<in> symKeys; ServKey \<in> symKeys;
Says A Tgs
- {|AuthTicket, (Crypt AuthKey {|Agent A, Number Ta1|}),
+ {|AuthTicket, Crypt AuthKey {|Agent A, Number Ta1|},
Agent B|}
\<in> set evs5;
Says Tgs' A
@@ -242,7 +243,7 @@
(*---------------------------------------------------------------------*)
-declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
declare parts.Body [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
@@ -260,7 +261,7 @@
apply (induct_tac [2] "a", auto)
done
-lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
+lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
(if A:bad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
apply (induct_tac [2] "a", auto)
@@ -290,30 +291,30 @@
apply (simp (no_asm))
done
-lemma AuthKeys_not_insert:
- "(\<forall>A Tk akey Peer.
- ev \<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,
- (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))
+lemma AuthKeys_not_insert:
+ "(\<forall>A Tk akey Peer.
+ ev \<noteq> Says Kas A (Crypt (shrK A) {|akey, Agent Peer, Tk,
+ (Crypt (shrK Peer) {|Agent A, Agent Peer, akey, Tk|})|}))
==> AuthKeys (ev # evs) = AuthKeys evs"
by (unfold AuthKeys_def, auto)
-lemma AuthKeys_insert:
- "AuthKeys
- (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk,
- (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs)
+lemma AuthKeys_insert:
+ "AuthKeys
+ (Says Kas A (Crypt (shrK A) {|Key K, Agent Peer, Number Tk,
+ (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K, Number Tk|})|}) # evs)
= insert K (AuthKeys evs)"
by (unfold AuthKeys_def, auto)
-lemma AuthKeys_simp:
- "K \<in> AuthKeys
- (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk,
- (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs)
+lemma AuthKeys_simp:
+ "K \<in> AuthKeys
+ (Says Kas A (Crypt (shrK A) {|Key K', Agent Peer, Number Tk,
+ (Crypt (shrK Peer) {|Agent A, Agent Peer, Key K', Number Tk|})|}) # evs)
==> K = K' | K \<in> AuthKeys evs"
by (unfold AuthKeys_def, auto)
-lemma AuthKeysI:
- "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk,
- (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \<in> set evs
+lemma AuthKeysI:
+ "Says Kas A (Crypt (shrK A) {|Key K, Agent Tgs, Number Tk,
+ (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key K, Number Tk|})|}) \<in> set evs
==> K \<in> AuthKeys evs"
by (unfold AuthKeys_def, auto)
@@ -325,34 +326,34 @@
text{*--For reasoning about the encrypted portion of message K3--*}
lemma K3_msg_in_parts_spies:
- "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|})
+ "Says Kas' A (Crypt KeyA {|AuthKey, Peer, Tk, AuthTicket|})
\<in> set evs ==> AuthTicket \<in> parts (spies evs)"
by blast
lemma Oops_range_spies1:
- "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|})
- \<in> set evs ;
- evs \<in> kerberos |] ==> AuthKey \<notin> range shrK"
+ "[| Says Kas A (Crypt KeyA {|Key AuthKey, Peer, Tk, AuthTicket|})
+ \<in> set evs ;
+ evs \<in> kerberos |] ==> AuthKey \<notin> range shrK & AuthKey \<in> symKeys"
apply (erule rev_mp)
apply (erule kerberos.induct, auto)
done
text{*--For reasoning about the encrypted portion of message K5--*}
lemma K5_msg_in_parts_spies:
- "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})
+ "Says Tgs' A (Crypt AuthKey {|ServKey, Agent B, Tt, ServTicket|})
\<in> set evs ==> ServTicket \<in> parts (spies evs)"
by blast
lemma Oops_range_spies2:
- "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
- \<in> set evs ;
- evs \<in> kerberos |] ==> ServKey \<notin> range shrK"
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ \<in> set evs ;
+ evs \<in> kerberos |] ==> ServKey \<notin> range shrK & ServKey \<in> symKeys"
apply (erule rev_mp)
apply (erule kerberos.induct, auto)
done
lemma Says_ticket_in_parts_spies:
- "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \<in> set evs
+ "Says S A (Crypt K {|SesKey, B, TimeStamp, Ticket|}) \<in> set evs
==> Ticket \<in> parts (spies evs)"
by blast
@@ -360,9 +361,9 @@
(*Spy never sees another agent's shared key! (unless it's lost at start)*)
lemma Spy_see_shrK [simp]:
"evs \<in> kerberos ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply (blast+)
done
@@ -376,22 +377,25 @@
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
text{*Nobody can have used non-existent keys!*}
-lemma new_keys_not_used [rule_format, simp]:
- "evs \<in> kerberos ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (spies evs))"
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+lemma new_keys_not_used [simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerberos|]
+ ==> K \<notin> keysFor (parts (spies evs))"
+apply (erule rev_mp)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake*}
apply (force dest!: keysFor_parts_insert)
txt{*Others*}
-apply (blast+)
+apply (force dest!: analz_shrK_Decrypt)+
done
-(*Earlier, all protocol proofs declared this theorem.
+(*Earlier, all protocol proofs declared this theorem.
But few of them actually need it! (Another is Yahalom) *)
lemma new_keys_not_analzd:
- "[|evs \<in> kerberos; Key K \<notin> used evs|] ==> K \<notin> keysFor (analz (spies evs))"
-by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
+ "[|evs \<in> kerberos; K \<in> symKeys; Key K \<notin> used evs|]
+ ==> K \<notin> keysFor (analz (spies evs))"
+by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
subsection{*Regularity Lemmas*}
@@ -399,11 +403,11 @@
text{*Describes the form of AuthKey, AuthTicket, and K sent by Kas*}
lemma Says_Kas_message_form:
- "[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|})
- \<in> set evs;
- evs \<in> kerberos |]
- ==> AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs &
- AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}) &
+ "[| Says Kas A (Crypt K {|Key AuthKey, Agent Peer, Tk, AuthTicket|})
+ \<in> set evs;
+ evs \<in> kerberos |]
+ ==> AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs & AuthKey \<in> symKeys &
+ AuthTicket = (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}) &
K = shrK A & Peer = Tgs"
apply (erule rev_mp)
apply (erule kerberos.induct)
@@ -411,8 +415,8 @@
apply (blast+)
done
-(*This lemma is essential for proving Says_Tgs_message_form:
-
+(*This lemma is essential for proving Says_Tgs_message_form:
+
the session key AuthKey
supplied by Kas in the authentication ticket
cannot be a long-term key!
@@ -420,35 +424,35 @@
Generalised to any session keys (both AuthKey and ServKey).
*)
lemma SesKey_is_session_key:
- "[| Crypt (shrK Tgs_B) {|Agent A, Agent Tgs_B, Key SesKey, Number T|}
- \<in> parts (spies evs); Tgs_B \<notin> bad;
- evs \<in> kerberos |]
+ "[| Crypt (shrK Tgs_B) {|Agent A, Agent Tgs_B, Key SesKey, Number T|}
+ \<in> parts (spies evs); Tgs_B \<notin> bad;
+ evs \<in> kerberos |]
==> SesKey \<notin> range shrK"
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
done
lemma A_trusts_AuthTicket:
- "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
- \<in> parts (spies evs);
- evs \<in> kerberos |]
- ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk,
- Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})
+ "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
+ \<in> parts (spies evs);
+ evs \<in> kerberos |]
+ ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk,
+ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}|})
\<in> set evs"
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake, K4*}
apply (blast+)
done
lemma AuthTicket_crypt_AuthKey:
- "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}
- \<in> parts (spies evs);
- evs \<in> kerberos |]
+ "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Number Tk|}
+ \<in> parts (spies evs);
+ evs \<in> kerberos |]
==> AuthKey \<in> AuthKeys evs"
apply (frule A_trusts_AuthTicket, assumption)
apply (simp (no_asm) add: AuthKeys_def)
@@ -457,12 +461,13 @@
text{*Describes the form of ServKey, ServTicket and AuthKey sent by Tgs*}
lemma Says_Tgs_message_form:
- "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
- \<in> set evs;
- evs \<in> kerberos |]
- ==> B \<noteq> Tgs & ServKey \<notin> range shrK & ServKey \<notin> AuthKeys evs &
- ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) &
- AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs"
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ \<in> set evs;
+ evs \<in> kerberos |]
+ ==> B \<noteq> Tgs &
+ ServKey \<notin> range shrK & ServKey \<notin> AuthKeys evs & ServKey \<in> symKeys &
+ ServTicket = (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|}) &
+ AuthKey \<notin> range shrK & AuthKey \<in> AuthKeys evs & AuthKey \<in> symKeys"
apply (erule rev_mp)
apply (erule kerberos.induct)
apply (simp_all add: AuthKeys_insert AuthKeys_not_insert AuthKeys_empty AuthKeys_simp, blast, auto)
@@ -472,18 +477,18 @@
apply (blast dest: AuthTicket_crypt_AuthKey)
done
-text{*Authenticity of AuthKey for A:
+text{*Authenticity of AuthKey for A:
If a certain encrypted message appears then it originated with Kas*}
lemma A_trusts_AuthKey:
- "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}
- \<in> parts (spies evs);
- A \<notin> bad; evs \<in> kerberos |]
- ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})
+ "[| Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|}
+ \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> kerberos |]
+ ==> Says Kas A (Crypt (shrK A) {|Key AuthKey, Peer, Tk, AuthTicket|})
\<in> set evs"
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake*}
apply blast
txt{*K4*}
@@ -493,18 +498,18 @@
text{*If a certain encrypted message appears then it originated with Tgs*}
lemma A_trusts_K4:
- "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
- \<in> parts (spies evs);
- Key AuthKey \<notin> analz (spies evs);
- AuthKey \<notin> range shrK;
- evs \<in> kerberos |]
- ==> \<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
+ \<in> parts (spies evs);
+ Key AuthKey \<notin> analz (spies evs);
+ AuthKey \<notin> range shrK;
+ evs \<in> kerberos |]
+ ==> \<exists>A. Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
\<in> set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake*}
apply blast
txt{*K2*}
@@ -514,55 +519,60 @@
done
lemma AuthTicket_form:
- "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}
- \<in> parts (spies evs);
- A \<notin> bad;
- evs \<in> kerberos |]
- ==> AuthKey \<notin> range shrK &
+ "[| Crypt (shrK A) {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}
+ \<in> parts (spies evs);
+ A \<notin> bad;
+ evs \<in> kerberos |]
+ ==> AuthKey \<notin> range shrK & AuthKey \<in> symKeys &
AuthTicket = Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}"
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
apply (blast+)
done
-text{* This form holds also over an AuthTicket, but is not needed below. *}
+text{* This form holds also over an AuthTicket, but is not needed below.*}
lemma ServTicket_form:
- "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
- \<in> parts (spies evs);
- Key AuthKey \<notin> analz (spies evs);
- evs \<in> kerberos |]
- ==> ServKey \<notin> range shrK &
+ "[| Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|}
+ \<in> parts (spies evs);
+ Key AuthKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
+ ==> ServKey \<notin> range shrK & ServKey \<in> symKeys &
(\<exists>A. ServTicket = Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
done
text{* Essentially the same as @{text AuthTicket_form} *}
lemma Says_kas_message_form:
- "[| Says Kas' A (Crypt (shrK A)
- {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \<in> set evs;
- evs \<in> kerberos |]
- ==> AuthKey \<notin> range shrK &
- AuthTicket =
- Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
+ "[| Says Kas' A (Crypt (shrK A)
+ {|Key AuthKey, Agent Tgs, Tk, AuthTicket|}) \<in> set evs;
+ evs \<in> kerberos |]
+ ==> AuthKey \<notin> range shrK & AuthKey \<in> symKeys &
+ AuthTicket =
+ Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, Tk|}
| AuthTicket \<in> analz (spies evs)"
-by (blast dest: Says_imp_spies [THEN analz.Inj] AuthTicket_form)
+by (blast dest: analz_shrK_Decrypt AuthTicket_form
+ Says_imp_spies [THEN analz.Inj])
+
lemma Says_tgs_message_form:
- "[| Says Tgs' A (Crypt AuthKey
- {|Key ServKey, Agent B, Tt, ServTicket|}) \<in> set evs;
- evs \<in> kerberos |]
- ==> ServKey \<notin> range shrK &
- (\<exists>A. ServTicket =
- Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})
- | ServTicket \<in> analz (spies evs)"
-by (blast dest: Says_imp_spies [THEN analz.Inj] ServTicket_form)
-
+ "[| Says Tgs' A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})
+ \<in> set evs; AuthKey \<in> symKeys;
+ evs \<in> kerberos |]
+ ==> ServKey \<notin> range shrK &
+ (\<exists>A. ServTicket =
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Tt|})
+ | ServTicket \<in> analz (spies evs)"
+apply (frule Says_imp_spies [THEN analz.Inj], auto)
+ apply (force dest!: ServTicket_form)
+apply (frule analz_into_parts)
+apply (frule ServTicket_form, auto)
+done
subsection{*Unicity Theorems*}
@@ -571,18 +581,18 @@
also Tgs in the place of B. *}
lemma unique_CryptKey:
- "[| Crypt (shrK B) {|Agent A, Agent B, Key SesKey, T|}
- \<in> parts (spies evs);
- Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}
- \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
- evs \<in> kerberos |]
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key SesKey, T|}
+ \<in> parts (spies evs);
+ Crypt (shrK B') {|Agent A', Agent B', Key SesKey, T'|}
+ \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
==> A=A' & B=B' & T=T'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake, K2, K4*}
apply (blast+)
done
@@ -591,18 +601,18 @@
A ServKey is encrypted by one and only one AuthKey.
*}
lemma Key_unique_SesKey:
- "[| Crypt K {|Key SesKey, Agent B, T, Ticket|}
- \<in> parts (spies evs);
- Crypt K' {|Key SesKey, Agent B', T', Ticket'|}
- \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
- evs \<in> kerberos |]
+ "[| Crypt K {|Key SesKey, Agent B, T, Ticket|}
+ \<in> parts (spies evs);
+ Crypt K' {|Key SesKey, Agent B', T', Ticket'|}
+ \<in> parts (spies evs); Key SesKey \<notin> analz (spies evs);
+ evs \<in> kerberos |]
==> K=K' & B=B' & T=T' & Ticket=Ticket'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake, K2, K4*}
apply (blast+)
done
@@ -612,47 +622,47 @@
At reception of any message mentioning A, Kas associates shrK A with
a new AuthKey. Realistic, as the user gets a new AuthKey at each login.
Similarly, at reception of any message mentioning an AuthKey
- (a legitimate user could make several requests to Tgs - by K3), Tgs
+ (a legitimate user could make several requests to Tgs - by K3), Tgs
associates it with a new ServKey.
Therefore, a goal like
- "evs \<in> kerberos
- ==> Key Kc \<notin> analz (spies evs) -->
- (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket.
- Crypt Kc {|Key K, Agent B, T, Ticket|}
+ "evs \<in> kerberos
+ ==> Key Kc \<notin> analz (spies evs) -->
+ (\<exists>K' B' T' Ticket'. \<forall>K B T Ticket.
+ Crypt Kc {|Key K, Agent B, T, Ticket|}
\<in> parts (spies evs) --> K=K' & B=B' & T=T' & Ticket=Ticket')"
would fail on the K2 and K4 cases.
*)
lemma unique_AuthKeys:
- "[| Says Kas A
- (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \<in> set evs;
- Says Kas A'
- (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) \<in> set evs;
+ "[| Says Kas A
+ (Crypt Ka {|Key AuthKey, Agent Tgs, Tk, X|}) \<in> set evs;
+ Says Kas A'
+ (Crypt Ka' {|Key AuthKey, Agent Tgs, Tk', X'|}) \<in> set evs;
evs \<in> kerberos |] ==> A=A' & Ka=Ka' & Tk=Tk' & X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*K2*}
apply blast
done
text{* ServKey uniquely identifies the message from Tgs *}
lemma unique_ServKeys:
- "[| Says Tgs A
- (Crypt K {|Key ServKey, Agent B, Tt, X|}) \<in> set evs;
- Says Tgs A'
- (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) \<in> set evs;
+ "[| Says Tgs A
+ (Crypt K {|Key ServKey, Agent B, Tt, X|}) \<in> set evs;
+ Says Tgs A'
+ (Crypt K' {|Key ServKey, Agent B', Tt', X'|}) \<in> set evs;
evs \<in> kerberos |] ==> A=A' & B=B' & K=K' & Tt=Tt' & X=X'"
apply (erule rev_mp)
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*K4*}
apply blast
done
@@ -663,19 +673,19 @@
lemma not_KeyCryptKey_Nil [iff]: "~ KeyCryptKey AuthKey ServKey []"
by (simp add: KeyCryptKey_def)
-lemma KeyCryptKeyI:
- "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \<in> set evs;
+lemma KeyCryptKeyI:
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \<in> set evs;
evs \<in> kerberos |] ==> KeyCryptKey AuthKey ServKey evs"
apply (unfold KeyCryptKey_def)
apply (blast dest: Says_Tgs_message_form)
done
-lemma KeyCryptKey_Says [simp]:
- "KeyCryptKey AuthKey ServKey (Says S A X # evs) =
- (Tgs = S &
- (\<exists>B tt. X = Crypt AuthKey
- {|Key ServKey, Agent B, tt,
- Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
+lemma KeyCryptKey_Says [simp]:
+ "KeyCryptKey AuthKey ServKey (Says S A X # evs) =
+ (Tgs = S &
+ (\<exists>B tt. X = Crypt AuthKey
+ {|Key ServKey, Agent B, tt,
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
| KeyCryptKey AuthKey ServKey evs)"
apply (unfold KeyCryptKey_def)
apply (simp (no_asm))
@@ -684,33 +694,33 @@
(*A fresh AuthKey cannot be associated with any other
(with respect to a given trace). *)
-lemma Auth_fresh_not_KeyCryptKey:
- "[| Key AuthKey \<notin> used evs; evs \<in> kerberos |]
+lemma Auth_fresh_not_KeyCryptKey:
+ "[| Key AuthKey \<notin> used evs; evs \<in> kerberos |]
==> ~ KeyCryptKey AuthKey ServKey evs"
apply (unfold KeyCryptKey_def)
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
done
(*A fresh ServKey cannot be associated with any other
(with respect to a given trace). *)
-lemma Serv_fresh_not_KeyCryptKey:
+lemma Serv_fresh_not_KeyCryptKey:
"Key ServKey \<notin> used evs ==> ~ KeyCryptKey AuthKey ServKey evs"
apply (unfold KeyCryptKey_def, blast)
done
lemma AuthKey_not_KeyCryptKey:
- "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}
- \<in> parts (spies evs); evs \<in> kerberos |]
+ "[| Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, tk|}
+ \<in> parts (spies evs); evs \<in> kerberos |]
==> ~ KeyCryptKey K AuthKey evs"
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
txt{*Fake*}
-apply blast
+apply blast
txt{*K2: by freshness*}
apply (simp add: KeyCryptKey_def)
txt{*K4*}
@@ -718,59 +728,59 @@
done
text{*A secure serverkey cannot have been used to encrypt others*}
-lemma ServKey_not_KeyCryptKey:
- "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \<in> parts (spies evs);
- Key SK \<notin> analz (spies evs);
- B \<noteq> Tgs; evs \<in> kerberos |]
+lemma ServKey_not_KeyCryptKey:
+ "[| Crypt (shrK B) {|Agent A, Agent B, Key SK, tt|} \<in> parts (spies evs);
+ Key SK \<notin> analz (spies evs); SK \<in> symKeys;
+ B \<noteq> Tgs; evs \<in> kerberos |]
==> ~ KeyCryptKey SK K evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerberos.induct, analz_mono_contra)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
txt{*K4 splits into distinct subcases*}
apply auto
txt{*ServKey can't have been enclosed in two certificates*}
prefer 2 apply (blast dest: unique_CryptKey)
-txt{*ServKey is fresh and so could not have been used, by
+txt{*ServKey is fresh and so could not have been used, by
@{text new_keys_not_used}*}
apply (force dest!: Crypt_imp_invKey_keysFor simp add: KeyCryptKey_def)
done
text{*Long term keys are not issued as ServKeys*}
-lemma shrK_not_KeyCryptKey:
+lemma shrK_not_KeyCryptKey:
"evs \<in> kerberos ==> ~ KeyCryptKey K (shrK A) evs"
apply (unfold KeyCryptKey_def)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (frule_tac [5] K3_msg_in_parts_spies, auto)
done
-text{*The Tgs message associates ServKey with AuthKey and therefore not with any
+text{*The Tgs message associates ServKey with AuthKey and therefore not with any
other key AuthKey.*}
-lemma Says_Tgs_KeyCryptKey:
- "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |})
- \<in> set evs;
- AuthKey' \<noteq> AuthKey; evs \<in> kerberos |]
+lemma Says_Tgs_KeyCryptKey:
+ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |})
+ \<in> set evs;
+ AuthKey' \<noteq> AuthKey; evs \<in> kerberos |]
==> ~ KeyCryptKey AuthKey' ServKey evs"
apply (unfold KeyCryptKey_def)
apply (blast dest: unique_ServKeys)
done
lemma KeyCryptKey_not_KeyCryptKey:
- "[| KeyCryptKey AuthKey ServKey evs; evs \<in> kerberos |]
+ "[| KeyCryptKey AuthKey ServKey evs; evs \<in> kerberos |]
==> ~ KeyCryptKey ServKey K evs"
apply (erule rev_mp)
-apply (erule kerberos.induct)
-apply (frule_tac [7] K5_msg_in_parts_spies)
+apply (erule kerberos.induct)
+apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, safe)
txt{*K4 splits into subcases*}
apply simp_all
prefer 4 apply (blast dest!: AuthKey_not_KeyCryptKey)
-txt{*ServKey is fresh and so could not have been used, by
+txt{*ServKey is fresh and so could not have been used, by
@{text new_keys_not_used}*}
- prefer 2
- apply (force dest!: Says_imp_spies [THEN parts.Inj] Crypt_imp_invKey_keysFor simp add: KeyCryptKey_def)
+ prefer 2
+ apply (force dest!: Crypt_imp_invKey_keysFor simp add: KeyCryptKey_def)
txt{*Others by freshness*}
apply (blast+)
done
@@ -781,30 +791,29 @@
text{*We take some pains to express the property
as a logical equivalence so that the simplifier can apply it.*}
lemma Key_analz_image_Key_lemma:
- "P --> (Key K \<in> analz (Key`KK Un H)) --> (K:KK | Key K \<in> analz H)
- ==>
+ "P --> (Key K \<in> analz (Key`KK Un H)) --> (K:KK | Key K \<in> analz H)
+ ==>
P --> (Key K \<in> analz (Key`KK Un H)) = (K:KK | Key K \<in> analz H)"
by (blast intro: analz_mono [THEN subsetD])
lemma KeyCryptKey_analz_insert:
- "[| KeyCryptKey K K' evs; evs \<in> kerberos |]
+ "[| KeyCryptKey K K' evs; K \<in> symKeys; evs \<in> kerberos |]
==> Key K' \<in> analz (insert (Key K) (spies evs))"
-apply (simp (no_asm_use) add: KeyCryptKey_def)
-apply clarify
+apply (simp add: KeyCryptKey_def, clarify)
apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto)
done
lemma AuthKeys_are_not_KeyCryptKey:
- "[| K \<in> AuthKeys evs Un range shrK; evs \<in> kerberos |]
+ "[| K \<in> AuthKeys evs Un range shrK; evs \<in> kerberos |]
==> \<forall>SK. ~ KeyCryptKey SK K evs"
apply (simp add: KeyCryptKey_def)
apply (blast dest: Says_Tgs_message_form)
done
lemma not_AuthKeys_not_KeyCryptKey:
- "[| K \<notin> AuthKeys evs;
- K \<notin> range shrK; evs \<in> kerberos |]
+ "[| K \<notin> AuthKeys evs;
+ K \<notin> range shrK; evs \<in> kerberos |]
==> \<forall>SK. ~ KeyCryptKey K SK evs"
apply (simp add: KeyCryptKey_def)
apply (blast dest: Says_Tgs_message_form)
@@ -815,10 +824,10 @@
text{*For the Oops2 case of the next theorem*}
lemma Oops2_not_KeyCryptKey:
- "[| evs \<in> kerberos;
- Says Tgs A (Crypt AuthKey
- {|Key ServKey, Agent B, Number Tt, ServTicket|})
- \<in> set evs |]
+ "[| evs \<in> kerberos;
+ Says Tgs A (Crypt AuthKey
+ {|Key ServKey, Agent B, Number Tt, ServTicket|})
+ \<in> set evs |]
==> ~ KeyCryptKey ServKey SK evs"
apply (blast dest: KeyCryptKeyI KeyCryptKey_not_KeyCryptKey)
done
@@ -831,10 +840,10 @@
[simplified by LCP] *}
lemma Key_analz_image_Key [rule_format (no_asm)]:
"evs \<in> kerberos ==>
- (\<forall>SK KK. KK <= -(range shrK) -->
- (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs) -->
- (Key SK \<in> analz (Key`KK Un (spies evs))) =
- (SK \<in> KK | Key SK \<in> analz (spies evs)))"
+ (\<forall>SK KK. SK \<in> symKeys & KK <= -(range shrK) -->
+ (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs) -->
+ (Key SK \<in> analz (Key`KK Un (spies evs))) =
+ (SK \<in> KK | Key SK \<in> analz (spies evs)))"
apply (erule kerberos.induct)
apply (frule_tac [10] Oops_range_spies2)
apply (frule_tac [9] Oops_range_spies1)
@@ -845,13 +854,17 @@
the induction hypothesis*}
apply (case_tac [11] "KeyCryptKey AuthKey SK evsO1")
apply (case_tac [8] "KeyCryptKey ServKey SK evs5")
-apply (simp_all del: image_insert
+apply (simp_all del: image_insert
add: analz_image_freshK_simps KeyCryptKey_Says shrK_not_KeyCryptKey
- Oops2_not_KeyCryptKey Auth_fresh_not_KeyCryptKey
+ Oops2_not_KeyCryptKey Auth_fresh_not_KeyCryptKey
Serv_fresh_not_KeyCryptKey Says_Tgs_KeyCryptKey Spy_analz_shrK)
--{*18 seconds on a 1.8GHz machine??*}
-txt{*Fake*}
+txt{*Fake*}
apply spy_analz
+txt{*K2*}
+apply blast
+txt{*K3*}
+apply blast
txt{*K4*}
apply (blast dest!: AuthKey_not_KeyCryptKey)
txt{*K5*}
@@ -861,32 +874,35 @@
txt{*...therefore ServKey is uncompromised.*}
txt{*The KeyCryptKey ServKey SK evs5 case leads to a contradiction.*}
apply (blast elim!: ServKey_not_KeyCryptKey [THEN [2] rev_notE] del: allE ballE)
+txt{*Another K5 case*}
+apply blast
txt{*Oops1*}
-apply simp
+apply simp
apply (blast dest!: KeyCryptKey_analz_insert)
done
-
text{* First simplification law for analz: no session keys encrypt
authentication keys or shared keys. *}
lemma analz_insert_freshK1:
"[| evs \<in> kerberos; K \<in> (AuthKeys evs) Un range shrK;
+ K \<in> symKeys;
SesKey \<notin> range shrK |]
==> (Key K \<in> analz (insert (Key SesKey) (spies evs))) =
(K = SesKey | Key K \<in> analz (spies evs))"
apply (frule AuthKeys_are_not_KeyCryptKey, assumption)
-apply (simp del: image_insert
+apply (simp del: image_insert
add: analz_image_freshK_simps add: Key_analz_image_Key)
done
text{* Second simplification law for analz: no service keys encrypt any other keys.*}
lemma analz_insert_freshK2:
- "[| evs \<in> kerberos; ServKey \<notin> (AuthKeys evs); ServKey \<notin> range shrK|]
+ "[| evs \<in> kerberos; ServKey \<notin> (AuthKeys evs); ServKey \<notin> range shrK;
+ K \<in> symKeys|]
==> (Key K \<in> analz (insert (Key ServKey) (spies evs))) =
(K = ServKey | Key K \<in> analz (spies evs))"
apply (frule not_AuthKeys_not_KeyCryptKey, assumption, assumption)
-apply (simp del: image_insert
+apply (simp del: image_insert
add: analz_image_freshK_simps add: Key_analz_image_Key)
done
@@ -896,12 +912,12 @@
lemma analz_insert_freshK3:
"[| Says Tgs A
(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
- \<in> set evs;
- AuthKey \<noteq> AuthKey'; AuthKey' \<notin> range shrK; evs \<in> kerberos |]
+ \<in> set evs; ServKey \<in> symKeys;
+ AuthKey \<noteq> AuthKey'; AuthKey' \<notin> range shrK; evs \<in> kerberos |]
==> (Key ServKey \<in> analz (insert (Key AuthKey') (spies evs))) =
(ServKey = AuthKey' | Key ServKey \<in> analz (spies evs))"
-apply (drule_tac AuthKey' = "AuthKey'" in Says_Tgs_KeyCryptKey, blast, assumption)
-apply (simp del: image_insert
+apply (drule_tac AuthKey' = AuthKey' in Says_Tgs_KeyCryptKey, blast, assumption)
+apply (simp del: image_insert
add: analz_image_freshK_simps add: Key_analz_image_Key)
done
@@ -910,11 +926,10 @@
lemma AuthKey_compromises_ServKey:
"[| Says Tgs A
(Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
- \<in> set evs;
+ \<in> set evs; AuthKey \<in> symKeys;
Key AuthKey \<in> analz (spies evs); evs \<in> kerberos |]
==> Key ServKey \<in> analz (spies evs)"
-apply (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
-done
+by (force dest: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst])
subsection{* Guarantees for Kas *}
@@ -938,7 +953,7 @@
text{*If Spy sees the Authentication Key sent in msg K2, then
the Key has expired.*}
lemma Confidentiality_Kas_lemma [rule_format]:
- "[| A \<notin> bad; evs \<in> kerberos |]
+ "[| AuthKey \<in> symKeys; A \<notin> bad; evs \<in> kerberos |]
==> Says Kas A
(Crypt (shrK A)
{|Key AuthKey, Agent Tgs, Number Tk,
@@ -967,7 +982,6 @@
apply (blast dest: Says_Tgs_message_form Says_Kas_message_form)
done
-
lemma Confidentiality_Kas:
"[| Says Kas A
(Crypt Ka {|Key AuthKey, Agent Tgs, Number Tk, AuthTicket|})
@@ -982,16 +996,18 @@
text{*If Spy sees the Service Key sent in msg K4, then
the Key has expired.*}
+
lemma Confidentiality_lemma [rule_format]:
"[| Says Tgs A
- (Crypt AuthKey
- {|Key ServKey, Agent B, Number Tt,
- Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})
- \<in> set evs;
- Key AuthKey \<notin> analz (spies evs);
- A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
- ==> Key ServKey \<in> analz (spies evs) -->
- ExpirServ Tt evs"
+ (Crypt AuthKey
+ {|Key ServKey, Agent B, Number Tt,
+ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|})
+ \<in> set evs;
+ Key AuthKey \<notin> analz (spies evs);
+ ServKey \<in> symKeys;
+ A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
+ ==> Key ServKey \<in> analz (spies evs) -->
+ ExpirServ Tt evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule kerberos.induct)
@@ -999,7 +1015,7 @@
--{*The Oops1 case is unusual: must simplify
@{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
@{text analz_mono_contra} weaken it to
- @{term "Authkey \<notin> analz (spies evs)"},
+ @{term "Authkey \<notin> analz (spies evs)"},
for we then conclude @{term "AuthKey \<noteq> AuthKeya"}.*}
apply analz_mono_contra
apply (frule_tac [10] Oops_range_spies2)
@@ -1018,11 +1034,11 @@
prefer 3
apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI)
txt{*Oops1*}
- prefer 2
+ prefer 2
apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI)
txt{*K5. Not clear how this step could be integrated with the main
simplification step.*}
-apply clarify
+apply clarify
apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl)
apply (frule Says_imp_spies [THEN parts.Inj, THEN ServKey_notin_AuthKeysD])
apply (assumption, blast, assumption)
@@ -1214,8 +1230,8 @@
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerberos |]
==> Key ServKey \<notin> analz (spies evs)"
apply (frule A_trusts_AuthKey)
-apply (frule_tac [3] Confidentiality_Kas)
-apply (frule_tac [6] B_trusts_ServTicket, auto)
+apply (frule_tac [3] Confidentiality_Kas)
+apply (frule_tac [6] B_trusts_ServTicket, auto)
apply (blast dest!: Confidentiality_Tgs2 dest: Says_Kas_message_form A_trusts_K4 unique_ServKeys unique_AuthKeys)
done
(*
@@ -1224,7 +1240,7 @@
Says_Kas_message_form B_trusts_ServTicket
unique_ServKeys unique_AuthKeys
Confidentiality_Kas
- Confidentiality_Tgs2)
+ Confidentiality_Tgs2)
It is very brittle: we can't use this command partway
through the script above.
*)
@@ -1449,8 +1465,7 @@
apply (erule rev_mp)
apply (erule kerberos.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
-apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
-apply blast
+apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast, blast)
apply (blast dest: Says_imp_spies [THEN parts.Inj, THEN A_trusts_AuthKey])
done
@@ -1492,14 +1507,14 @@
apply (frule_tac [7] Says_ticket_in_parts_spies)
apply (simp_all (no_asm_simp))
apply clarify
-txt{*K6*}
+txt{*K5*}
apply auto
apply (simp add: takeWhile_tail)
txt{*Level 15: case study necessary because the assumption doesn't state
the form of ServTicket. The guarantee becomes stronger.*}
-apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
- K3_imp_K2 K4_trustworthy'
- parts_spies_takeWhile_mono [THEN subsetD]
+apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
+ K3_imp_K2 K4_trustworthy'
+ parts_spies_takeWhile_mono [THEN subsetD]
parts_spies_evs_revD2 [THEN subsetD]
intro: Says_Auth)
apply (simp add: takeWhile_tail)
--- a/src/HOL/Auth/Kerberos_BAN.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Fri Sep 26 10:34:28 2003 +0200
@@ -3,22 +3,23 @@
Author: Giampaolo Bella, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-The Kerberos protocol, BAN version.
-
-From page 251 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-
- Confidentiality (secrecy) and authentication properties rely on
- temporal checks: strong guarantees in a little abstracted - but
- very realistic - model (see .thy).
-
Tidied and converted to Isar by lcp.
*)
-theory Kerberos_BAN = Shared:
+header{*The Kerberos Protocol, BAN Version*}
+
+theory Kerberos_BAN = Public:
-(* Temporal modelization: session keys can be leaked
+text{*From page 251 of
+ Burrows, Abadi and Needham (1989). A Logic of Authentication.
+ Proc. Royal Soc. 426
+
+ Confidentiality (secrecy) and authentication properties rely on
+ temporal checks: strong guarantees in a little abstracted - but
+ very realistic - model.
+*}
+
+(* Temporal modelization: session keys can be leaked
ONLY when they have expired *)
syntax
@@ -46,15 +47,15 @@
translations
- "CT" == "length"
-
+ "CT" == "length "
+
"Expired T evs" == "SesKeyLife + T < CT evs"
"RecentAuth T evs" == "CT evs \<le> AutLife + T"
consts kerberos_ban :: "event list set"
inductive "kerberos_ban"
- intros
+ intros
Nil: "[] \<in> kerberos_ban"
@@ -67,53 +68,53 @@
\<in> kerberos_ban"
- Kb2: "[| evs2 \<in> kerberos_ban; Key KAB \<notin> used evs2;
+ Kb2: "[| evs2 \<in> kerberos_ban; Key KAB \<notin> used evs2; KAB \<in> symKeys;
Says A' Server {|Agent A, Agent B|} \<in> set evs2 |]
- ==> Says Server A
+ ==> Says Server A
(Crypt (shrK A)
- {|Number (CT evs2), Agent B, Key KAB,
- (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|})
+ {|Number (CT evs2), Agent B, Key KAB,
+ (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|})
# evs2 \<in> kerberos_ban"
- Kb3: "[| evs3 \<in> kerberos_ban;
- Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ Kb3: "[| evs3 \<in> kerberos_ban;
+ Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
\<in> set evs3;
Says A Server {|Agent A, Agent B|} \<in> set evs3;
~ Expired Ts evs3 |]
- ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |}
+ ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |}
# evs3 \<in> kerberos_ban"
- Kb4: "[| evs4 \<in> kerberos_ban;
- Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
+ Kb4: "[| evs4 \<in> kerberos_ban;
+ Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}),
(Crypt K {|Agent A, Number Ta|}) |}: set evs4;
~ Expired Ts evs4; RecentAuth Ta evs4 |]
==> Says B A (Crypt K (Number Ta)) # evs4
\<in> kerberos_ban"
(*Old session keys may become compromised*)
- Oops: "[| evso \<in> kerberos_ban;
+ Oops: "[| evso \<in> kerberos_ban;
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
\<in> set evso;
Expired Ts evso |]
==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban"
-declare Says_imp_knows_Spy [THEN parts.Inj, dest]
+declare Says_imp_knows_Spy [THEN parts.Inj, dest]
declare parts.Body [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
-(*A "possibility property": there are traces that reach the end.*)
-lemma "Key K \<notin> used []
- ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban.
- Says B A (Crypt K (Number Timestamp))
+text{*A "possibility property": there are traces that reach the end.*}
+lemma "[|Key K \<notin> used []; K \<in> symKeys|]
+ ==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban.
+ Says B A (Crypt K (Number Timestamp))
\<in> set evs"
apply (cut_tac SesKeyLife_LB)
apply (intro exI bexI)
-apply (rule_tac [2]
- kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2,
+apply (rule_tac [2]
+ kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2,
THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4])
apply (possibility, simp_all (no_asm_simp) add: used_Cons)
done
@@ -121,114 +122,109 @@
(**** Inductive proofs about kerberos_ban ****)
-(*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
+text{*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*}
lemma Kb3_msg_in_parts_spies:
- "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs
+ "Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs
==> X \<in> parts (spies evs)"
by blast
-
+
lemma Oops_parts_spies:
- "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs
+ "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs
==> K \<in> parts (spies evs)"
by blast
-(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+text{*Spy never sees another agent's shared key! (unless it's bad at start)*}
lemma Spy_see_shrK [simp]:
"evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule kerberos_ban.induct)
-apply (frule_tac [7] Oops_parts_spies)
-apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
-apply blast+
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
"evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
-apply auto
-done
-
+by auto
lemma Spy_see_shrK_D [dest!]:
- "[| Key (shrK A) \<in> parts (spies evs);
+ "[| Key (shrK A) \<in> parts (spies evs);
evs \<in> kerberos_ban |] ==> A:bad"
-apply (blast dest: Spy_see_shrK)
-done
+by (blast dest: Spy_see_shrK)
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!]
-(*Nobody can have used non-existent keys!*)
-lemma new_keys_not_used [rule_format, simp]:
- "evs \<in> kerberos_ban ==>
- Key K \<notin> used evs --> K \<notin> keysFor (parts (spies evs))"
-apply (erule kerberos_ban.induct)
-apply (frule_tac [7] Oops_parts_spies)
-apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
-(*Fake*)
+text{*Nobody can have used non-existent keys!*}
+lemma new_keys_not_used [simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerberos_ban|]
+ ==> K \<notin> keysFor (parts (spies evs))"
+apply (erule rev_mp)
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+txt{*Fake*}
apply (force dest!: keysFor_parts_insert)
-(*Kb2, Kb3, Kb4*)
-apply blast+
+txt{*Kb2, Kb3, Kb4*}
+apply (force dest!: analz_shrK_Decrypt)+
done
-(** Lemmas concerning the form of items passed in messages **)
+subsection{* Lemmas concerning the form of items passed in messages *}
-(*Describes the form of K, X and K' when the Server sends this message.*)
+text{*Describes the form of K, X and K' when the Server sends this message.*}
lemma Says_Server_message_form:
- "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})
- \<in> set evs; evs \<in> kerberos_ban |]
- ==> K \<notin> range shrK &
- X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &
+ "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs; evs \<in> kerberos_ban |]
+ ==> K \<notin> range shrK &
+ X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) &
K' = shrK A"
apply (erule rev_mp)
apply (erule kerberos_ban.induct, auto)
done
-(*If the encrypted message appears then it originated with the Server
+text{*If the encrypted message appears then it originated with the Server
PROVIDED that A is NOT compromised!
This shows implicitly the FRESHNESS OF THE SESSION KEY to A
-*)
+*}
lemma A_trusts_K_by_Kb2:
- "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
- \<in> parts (spies evs);
- A \<notin> bad; evs \<in> kerberos_ban |]
- ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
+ \<in> parts (spies evs);
+ A \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
\<in> set evs"
apply (erule rev_mp)
-apply (erule kerberos_ban.induct)
-apply (frule_tac [7] Oops_parts_spies)
-apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
-apply blast
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast)
done
-(*If the TICKET appears then it originated with the Server*)
-(*FRESHNESS OF THE SESSION KEY to B*)
+text{*If the TICKET appears then it originated with the Server*}
+text{*FRESHNESS OF THE SESSION KEY to B*}
lemma B_trusts_K_by_Kb3:
- "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs);
- B \<notin> bad; evs \<in> kerberos_ban |]
- ==> Says Server A
- (Crypt (shrK A) {|Number Ts, Agent B, Key K,
- Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
+ "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs);
+ B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says Server A
+ (Crypt (shrK A) {|Number Ts, Agent B, Key K,
+ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
\<in> set evs"
apply (erule rev_mp)
-apply (erule kerberos_ban.induct)
-apply (frule_tac [7] Oops_parts_spies)
-apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
-apply blast
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast)
done
-(*EITHER describes the form of X when the following message is sent,
+text{*EITHER describes the form of X when the following message is sent,
OR reduces it to the Fake case.
- Use Says_Server_message_form if applicable.*)
+ Use @{text Says_Server_message_form} if applicable.*}
lemma Says_S_message_form:
- "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
- \<in> set evs;
- evs \<in> kerberos_ban |]
- ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))
+ "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs;
+ evs \<in> kerberos_ban |]
+ ==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}))
| X \<in> analz (spies evs)"
apply (case_tac "A \<in> bad")
apply (force dest!: Says_imp_spies [THEN analz.Inj])
@@ -248,56 +244,51 @@
****)
-
-(** Session keys are not used to encrypt other session keys **)
-
+text{* Session keys are not used to encrypt other session keys *}
lemma analz_image_freshK [rule_format (no_asm)]:
- "evs \<in> kerberos_ban ==>
- \<forall>K KK. KK \<subseteq> - (range shrK) -->
- (Key K \<in> analz (Key`KK Un (spies evs))) =
+ "evs \<in> kerberos_ban ==>
+ \<forall>K KK. KK \<subseteq> - (range shrK) -->
+ (Key K \<in> analz (Key`KK Un (spies evs))) =
(K \<in> KK | Key K \<in> analz (spies evs))"
apply (erule kerberos_ban.induct)
apply (drule_tac [7] Says_Server_message_form)
-apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
+apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto)
done
-
lemma analz_insert_freshK:
- "[| evs \<in> kerberos_ban; KAB \<notin> range shrK |] ==>
- (Key K \<in> analz (insert (Key KAB) (spies evs))) =
+ "[| evs \<in> kerberos_ban; KAB \<notin> range shrK |] ==>
+ (Key K \<in> analz (insert (Key KAB) (spies evs))) =
(K = KAB | Key K \<in> analz (spies evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)
-(** The session key K uniquely identifies the message **)
-
+text{* The session key K uniquely identifies the message *}
lemma unique_session_keys:
- "[| Says Server A
- (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs;
- Says Server A'
- (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs;
+ "[| Says Server A
+ (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs;
+ Says Server A'
+ (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs;
evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'"
apply (erule rev_mp)
apply (erule rev_mp)
-apply (erule kerberos_ban.induct)
-apply (frule_tac [7] Oops_parts_spies)
-apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
-(*Kb2: it can't be a new key*)
+apply (erule kerberos_ban.induct)
+apply (frule_tac [7] Oops_parts_spies)
+apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all)
+txt{*Kb2: it can't be a new key*}
apply blast
done
-(** Lemma: the session key sent in msg Kb2 would be EXPIRED
- if the spy could see it!
-**)
+text{* Lemma: the session key sent in msg Kb2 would be EXPIRED
+ if the spy could see it! *}
lemma lemma2 [rule_format (no_asm)]:
- "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
- ==> Says Server A
- (Crypt (shrK A) {|Number Ts, Agent B, Key K,
- Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
- \<in> set evs -->
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says Server A
+ (Crypt (shrK A) {|Number Ts, Agent B, Key K,
+ Crypt (shrK B) {|Number Ts, Agent A, Key K|}|})
+ \<in> set evs -->
Key K \<in> analz (spies evs) --> Expired Ts evs"
apply (erule kerberos_ban.induct)
apply (frule_tac [7] Says_Server_message_form)
@@ -316,54 +307,48 @@
done
-(** CONFIDENTIALITY for the SERVER:
- Spy does not see the keys sent in msg Kb2
- as long as they have NOT EXPIRED
-**)
+text{*Confidentiality for the Server: Spy does not see the keys sent in msg Kb2
+as long as they have not expired.*}
lemma Confidentiality_S:
- "[| Says Server A
- (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs;
- ~ Expired T evs;
- A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
+ "[| Says Server A
+ (Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs;
+ ~ Expired T evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
|] ==> Key K \<notin> analz (spies evs)"
apply (frule Says_Server_message_form, assumption)
apply (blast intro: lemma2)
done
-(**** THE COUNTERPART OF CONFIDENTIALITY
+(**** THE COUNTERPART OF CONFIDENTIALITY
[|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs)
WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****)
-(** CONFIDENTIALITY for ALICE: **)
-(** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
+text{*Confidentiality for Alice*}
lemma Confidentiality_A:
- "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs);
- ~ Expired T evs;
- A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
+ "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs);
+ ~ Expired T evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
|] ==> Key K \<notin> analz (spies evs)"
-apply (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S)
-done
+by (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S)
-(** CONFIDENTIALITY for BOB: **)
-(** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
+text{*Confidentiality for Bob*}
lemma Confidentiality_B:
- "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|}
- \<in> parts (spies evs);
- ~ Expired Tk evs;
- A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
+ "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|}
+ \<in> parts (spies evs);
+ ~ Expired Tk evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban
|] ==> Key K \<notin> analz (spies evs)"
-apply (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S)
-done
+by (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S)
lemma lemma_B [rule_format]:
- "[| B \<notin> bad; evs \<in> kerberos_ban |]
- ==> Key K \<notin> analz (spies evs) -->
- Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
- \<in> set evs -->
- Crypt K (Number Ta) \<in> parts (spies evs) -->
+ "[| B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Key K \<notin> analz (spies evs) -->
+ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs -->
+ Crypt K (Number Ta) \<in> parts (spies evs) -->
Says B A (Crypt K (Number Ta)) \<in> set evs"
apply (erule kerberos_ban.induct)
apply (frule_tac [7] Oops_parts_spies)
@@ -372,35 +357,33 @@
apply (simp_all (no_asm_simp) add: all_conj_distrib)
txt{*Fake*}
apply blast
-txt{*Kb2*}
-apply (force dest: Crypt_imp_invKey_keysFor)
+txt{*Kb2*}
+apply (force dest: Crypt_imp_invKey_keysFor)
txt{*Kb4*}
-apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys
+apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys
Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad)
done
-(*AUTHENTICATION OF B TO A*)
+text{*Authentication of B to A*}
lemma Authentication_B:
- "[| Crypt K (Number Ta) \<in> parts (spies evs);
- Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
- \<in> parts (spies evs);
- ~ Expired Ts evs;
- A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ "[| Crypt K (Number Ta) \<in> parts (spies evs);
+ Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}
+ \<in> parts (spies evs);
+ ~ Expired Ts evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
==> Says B A (Crypt K (Number Ta)) \<in> set evs"
by (blast dest!: A_trusts_K_by_Kb2
intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE])
-
-
lemma lemma_A [rule_format]:
- "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
- ==>
- Key K \<notin> analz (spies evs) -->
- Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
- \<in> set evs -->
- Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) -->
- Says A B {|X, Crypt K {|Agent A, Number Ta|}|}
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==>
+ Key K \<notin> analz (spies evs) -->
+ Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})
+ \<in> set evs -->
+ Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) -->
+ Says A B {|X, Crypt K {|Agent A, Number Ta|}|}
\<in> set evs"
apply (erule kerberos_ban.induct)
apply (frule_tac [7] Oops_parts_spies)
@@ -410,23 +393,22 @@
txt{*Fake*}
apply blast
txt{*Kb2*}
-apply (force dest: Crypt_imp_invKey_keysFor)
+apply (force dest: Crypt_imp_invKey_keysFor)
txt{*Kb3*}
apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys)
done
-
-(*AUTHENTICATION OF A TO B*)
+text{*Authentication of A to B*}
lemma Authentication_A:
- "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs);
- Crypt (shrK B) {|Number Ts, Agent A, Key K|}
- \<in> parts (spies evs);
- ~ Expired Ts evs;
- A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
- ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|},
+ "[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs);
+ Crypt (shrK B) {|Number Ts, Agent A, Key K|}
+ \<in> parts (spies evs);
+ ~ Expired Ts evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |]
+ ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|},
Crypt K {|Agent A, Number Ta|}|} \<in> set evs"
by (blast dest!: B_trusts_K_by_Kb3
- intro!: lemma_A
+ intro!: lemma_A
elim!: Confidentiality_S [THEN [2] rev_notE])
end
--- a/src/HOL/Auth/NS_Public.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/NS_Public.thy Fri Sep 26 10:34:28 2003 +0200
@@ -52,8 +52,7 @@
lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
- THEN ns_public.NS3])
-apply possibility
+ THEN ns_public.NS3], possibility)
done
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
--- a/src/HOL/Auth/NS_Shared.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,15 +2,17 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
-
-From page 247 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
*)
-theory NS_Shared = Shared:
+header{*The Needham-Schroeder Shared-Key Protocol*}
+
+theory NS_Shared = Public:
+
+text{*
+From page 247 of
+ Burrows, Abadi and Needham (1989). A Logic of Authentication.
+ Proc. Royal Soc. 426
+*}
consts ns_shared :: "event list set"
inductive "ns_shared"
@@ -31,7 +33,7 @@
!! It may respond more than once to A's request !!
Server doesn't know who the true sender is, hence the A' in
the sender field.*)
- NS2: "\<lbrakk>evs2 \<in> ns_shared; Key KAB \<notin> used evs2;
+ NS2: "\<lbrakk>evs2 \<in> ns_shared; Key KAB \<notin> used evs2; KAB \<in> symKeys;
Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
\<Longrightarrow> Says Server A
(Crypt (shrK A)
@@ -48,7 +50,7 @@
(*Bob's nonce exchange. He does not know who the message came
from, but responds to A because she is mentioned inside.*)
- NS4: "\<lbrakk>evs4 \<in> ns_shared; Nonce NB \<notin> used evs4;
+ NS4: "\<lbrakk>evs4 \<in> ns_shared; Nonce NB \<notin> used evs4; K \<in> symKeys;
Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
\<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
@@ -57,7 +59,7 @@
We do NOT send NB-1 or similar as the Spy cannot spoof such things.
Letting the Spy add or subtract 1 lets him send all nonces.
Instead we distinguish the messages by sending the nonce twice.*)
- NS5: "\<lbrakk>evs5 \<in> ns_shared;
+ NS5: "\<lbrakk>evs5 \<in> ns_shared; K \<in> symKeys;
Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
\<in> set evs5\<rbrakk>
@@ -80,14 +82,14 @@
text{*A "possibility property": there are traces that reach the end*}
-lemma "[| A \<noteq> Server; Key K \<notin> used [] |]
+lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
==> \<exists>N. \<exists>evs \<in> ns_shared.
Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_shared.Nil
[THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
THEN ns_shared.NS4, THEN ns_shared.NS5])
-apply (possibility, simp add: used_Cons)
+apply (possibility, simp add: used_Cons)
done
(*This version is similar, while instantiating ?K and ?N to epsilon-terms
@@ -126,8 +128,10 @@
text{*Nobody can have used non-existent keys!*}
-lemma new_keys_not_used [rule_format, simp]:
- "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
+lemma new_keys_not_used [simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
+ ==> K \<notin> keysFor (parts (spies evs))"
+apply (erule rev_mp)
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
txt{*Fake, NS2, NS4, NS5*}
apply (force dest!: keysFor_parts_insert, blast+)
@@ -161,15 +165,15 @@
\<Longrightarrow> K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
-(*EITHER describes the form of X when the following message is sent,
+text{*EITHER describes the form of X when the following message is sent,
OR reduces it to the Fake case.
- Use Says_Server_message_form if applicable.*)
+ Use @{text Says_Server_message_form} if applicable.*}
lemma Says_S_message_form:
"\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
evs \<in> ns_shared\<rbrakk>
\<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
\<or> X \<in> analz (spies evs)"
-by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
+by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
(*Alternative version also provable
@@ -216,9 +220,11 @@
\<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
(Key K \<in> analz (Key`KK \<union> (spies evs))) =
(K \<in> KK \<or> Key K \<in> analz (spies evs))"
-apply (erule ns_shared.induct, force)
-apply (drule_tac [7] Says_Server_message_form)
-apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
+apply (erule ns_shared.induct)
+apply (drule_tac [8] Says_Server_message_form)
+apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
+txt{*NS2, NS3*}
+apply blast+;
done
@@ -255,10 +261,10 @@
apply (frule_tac [7] Says_Server_message_form)
apply (frule_tac [4] Says_S_message_form)
apply (erule_tac [5] disjE)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
txt{*NS2*}
apply blast
-txt{*NS3, Server sub-case*}
+txt{*NS3, Server sub-case*}
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
dest: Says_imp_knows_Spy analz.Inj unique_session_keys)
txt{*NS3, Spy sub-case; also Oops*}
@@ -298,13 +304,13 @@
Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
Says B A (Crypt K (Nonce NB)) \<in> set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply (analz_mono_contra, simp_all, blast)
-(*NS2: contradiction from the assumptions
- Key K \<notin> used evs2 and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
-apply (force dest!: Crypt_imp_keysFor)
+apply (analz_mono_contra, simp_all, blast)
+txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
+ @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *}
+apply (force dest!: Crypt_imp_keysFor)
txt{*NS3*}
-apply blast
-txt{*NS4*}
+apply blast
+txt{*NS4*}
apply (blast dest: B_trusts_NS3
Says_imp_knows_Spy [THEN analz.Inj]
Crypt_Spy_analz_bad unique_session_keys)
@@ -320,9 +326,9 @@
by (blast intro: A_trusts_NS4_lemma
dest: A_trusts_NS2 Spy_not_see_encrypted_key)
-(*If the session key has been used in NS4 then somebody has forwarded
+text{*If the session key has been used in NS4 then somebody has forwarded
component X in some instance of NS4. Perhaps an interesting property,
- but not needed (after all) for the proofs below.*)
+ but not needed (after all) for the proofs below.*}
theorem NS4_implies_NS3 [rule_format]:
"evs \<in> ns_shared \<Longrightarrow>
Key K \<notin> analz (spies evs) \<longrightarrow>
@@ -332,7 +338,7 @@
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
apply (simp_all add: ex_disj_distrib, blast)
txt{*NS2*}
-apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
txt{*NS3*}
apply blast
txt{*NS4*}
@@ -352,9 +358,9 @@
Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
txt{*NS2*}
-apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
txt{*NS3*}
-apply (blast dest!: cert_A_form)
+apply (blast dest!: cert_A_form)
txt{*NS5*}
apply (blast dest!: A_trusts_NS2
dest: Says_imp_knows_Spy [THEN analz.Inj]
--- a/src/HOL/Auth/OtwayRees.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,18 +2,17 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-
-From page 244 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
*)
-header{*Verifying the Otway-Rees protocol*}
+header{*The Original Otway-Rees Protocol*}
+
+theory OtwayRees = Public:
-theory OtwayRees = Shared:
+text{* From page 244 of
+ Burrows, Abadi and Needham (1989). A Logic of Authentication.
+ Proc. Royal Soc. 426
-text{*This is the original version, which encrypts Nonce NB.*}
+This is the original version, which encrypts Nonce NB.*}
consts otway :: "event list set"
inductive "otway"
@@ -180,10 +179,10 @@
\<forall>K KK. KK <= -(range shrK) -->
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
-apply (erule otway.induct, force)
-apply (frule_tac [7] Says_Server_message_form)
-apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
+apply (erule otway.induct)
+apply (frule_tac [8] Says_Server_message_form)
+apply (drule_tac [7] OR4_analz_knows_Spy)
+apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto)
done
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,10 +2,14 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
+*)
-Inductive relation "otway" for the Otway-Rees protocol.
+header{*The Otway-Rees Protocol as Modified by Abadi and Needham*}
-Abadi-Needham simplified version: minimal encryption, explicit messages
+theory OtwayRees_AN = Public:
+
+text{*
+This simplified version has minimal encryption and explicit messages.
Note that the formalization does not even assume that nonces are fresh.
This is because the protocol does not rely on uniqueness of nonces for
@@ -13,11 +17,10 @@
properties.
From page 11 of
- Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
- IEEE Trans. SE 22 (1), 1996
-*)
-
-theory OtwayRees_AN = Shared:
+ Abadi and Needham (1996).
+ Prudent Engineering Practice for Cryptographic Protocols.
+ IEEE Trans. SE 22 (1)
+*}
consts otway :: "event list set"
inductive "otway"
@@ -138,7 +141,7 @@
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
apply (erule rev_mp)
-apply (erule otway.induct, simp_all, blast)
+apply (erule otway.induct, auto)
done
@@ -161,9 +164,9 @@
\<forall>K KK. KK <= -(range shrK) -->
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
-apply (erule otway.induct, force)
-apply (frule_tac [7] Says_Server_message_form)
-apply (drule_tac [6] OR4_analz_knows_Spy, analz_freshK, spy_analz)
+apply (erule otway.induct)
+apply (frule_tac [8] Says_Server_message_form)
+apply (drule_tac [7] OR4_analz_knows_Spy, analz_freshK, spy_analz, auto)
done
lemma analz_insert_freshK:
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,20 +2,22 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
+*)
-Inductive relation "otway" for the Otway-Rees protocol.
+
+header{*The Otway-Rees Protocol: The Faulty BAN Version*}
-The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
+theory OtwayRees_Bad = Public:
+
+text{*The FAULTY version omitting encryption of Nonce NB, as suggested on
+page 247 of
+ Burrows, Abadi and Needham (1988). A Logic of Authentication.
+ Proc. Royal Soc. 426
This file illustrates the consequences of such errors. We can still prove
-impressive-looking properties such as Spy_not_see_encrypted_key, yet the
-protocol is open to a middleperson attack. Attempting to prove some key lemmas
-indicates the possibility of this attack.
-*)
-
-theory OtwayRees_Bad = Shared:
+impressive-looking properties such as @{text Spy_not_see_encrypted_key}, yet
+the protocol is open to a middleperson attack. Attempting to prove some key
+lemmas indicates the possibility of this attack.*}
consts otway :: "event list set"
inductive "otway"
@@ -184,10 +186,10 @@
\<forall>K KK. KK <= -(range shrK) -->
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
-apply (erule otway.induct, force)
-apply (frule_tac [7] Says_Server_message_form)
-apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
+apply (erule otway.induct)
+apply (frule_tac [8] Says_Server_message_form)
+apply (drule_tac [7] OR4_analz_knows_Spy)
+apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto)
done
lemma analz_insert_freshK:
--- a/src/HOL/Auth/Public.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Public.thy Fri Sep 26 10:34:28 2003 +0200
@@ -10,6 +10,9 @@
theory Public = Event:
+lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
+by (simp add: symKeys_def)
+
subsection{*Asymmetric Keys*}
consts
@@ -51,8 +54,7 @@
injective_publicKey:
"publicKey b A = publicKey c A' ==> b=c & A=A'"
apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"])
- apply (auto simp add: inj_on_def split: agent.split)
- apply presburger+
+ apply (auto simp add: inj_on_def split: agent.split, presburger+)
(*faster would be this:
apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
*)
@@ -137,6 +139,17 @@
(*Injectiveness: Agents' long-term keys are distinct.*)
declare inj_shrK [THEN inj_eq, iff]
+lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
+by (simp add: invKey_K)
+
+lemma analz_shrK_Decrypt:
+ "[| Crypt (shrK A) X \<in> analz H; Key(shrK A) \<in> analz H |] ==> X \<in> analz H"
+by auto
+
+lemma analz_Decrypt':
+ "[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] ==> X \<in> analz H"
+by (auto simp add: invKey_K)
+
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C"
by (simp add: symKeys_neq_imp_neq)
@@ -165,6 +178,9 @@
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)"
by auto
+text{*For some reason, moving this up can make some proofs loop!*}
+declare invKey_K [simp]
+
subsection{*Initial States of Agents*}
@@ -233,7 +249,6 @@
lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []"
by (simp add: Crypt_notin_initState used_Nil)
-
(*** Basic properties of shrK ***)
(*Agents see their own shared keys!*)
@@ -246,16 +261,18 @@
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs"
by (rule initState_into_used, blast)
+
(** Fresh keys never clash with long-term shared keys **)
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
from long-term shared keys*)
-lemma Key_not_used: "Key K \<notin> used evs ==> K \<notin> range shrK"
+lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK"
by blast
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K"
by blast
+declare shrK_neq [THEN not_sym, simp]
subsection{*Function @{term spies} *}
@@ -300,6 +317,12 @@
apply(rule priK_in_initState [THEN parts.Inj])
done
+(*For case analysis on whether or not an agent is compromised*)
+lemma Crypt_Spy_analz_bad:
+ "[| Crypt (shrK A) X \<in> analz (knows Spy evs); A \<in> bad |]
+ ==> X \<in> analz (knows Spy evs)"
+by force
+
subsection{*Fresh Nonces*}
@@ -344,36 +367,48 @@
val insert_Key_image = thm "insert_Key_image";
*}
-(*
-val not_symKeys_pubK = thm "not_symKeys_pubK";
-val not_symKeys_priK = thm "not_symKeys_priK";
-val symKeys_neq_imp_neq = thm "symKeys_neq_imp_neq";
-val analz_symKeys_Decrypt = thm "analz_symKeys_Decrypt";
-val invKey_image_eq = thm "invKey_image_eq";
-val pubK_image_eq = thm "pubK_image_eq";
-val priK_pubK_image_eq = thm "priK_pubK_image_eq";
-val keysFor_parts_initState = thm "keysFor_parts_initState";
-val priK_in_initState = thm "priK_in_initState";
-val spies_pubK = thm "spies_pubK";
-val Spy_spies_bad = thm "Spy_spies_bad";
-val Nonce_notin_initState = thm "Nonce_notin_initState";
-val Nonce_notin_used_empty = thm "Nonce_notin_used_empty";
-*)
-
-
-lemma invKey_K [simp]: "K \<in> symKeys ==> invKey K = K"
-by (simp add: symKeys_def)
-
-lemma Crypt_imp_keysFor :"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
+lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)
+text{*Lemma for the trivial direction of the if-and-only-if of the
+Session Key Compromise Theorem*}
+lemma analz_image_freshK_lemma:
+ "(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H) ==>
+ (Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)"
+by (blast intro: analz_mono [THEN [2] rev_subsetD])
+
+lemmas analz_image_freshK_simps =
+ simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
+ disj_comms
+ image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
+ analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
+ insert_Key_singleton
+ Key_not_used insert_Key_image Un_assoc [THEN sym]
+
+ML
+{*
+val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
+val analz_image_freshK_simps = thms "analz_image_freshK_simps";
+
+val analz_image_freshK_ss =
+ simpset() delsimps [image_insert, image_Un]
+ delsimps [imp_disjL] (*reduces blow-up*)
+ addsimps thms "analz_image_freshK_simps"
+*}
+
+method_setup analz_freshK = {*
+ Method.no_args
+ (Method.METHOD
+ (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
+ REPEAT_FIRST (rtac analz_image_freshK_lemma),
+ ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *}
+ "for proving the Session Key Compromise theorem"
subsection{*Specialized Methods for Possibility Theorems*}
ML
{*
-val Nonce_supply1 = thm "Nonce_supply1";
val Nonce_supply = thm "Nonce_supply";
(*Tactic for possibility theorems (Isar interface)*)
@@ -386,6 +421,14 @@
(*Tactic for possibility theorems (ML script version)*)
fun possibility_tac state = gen_possibility_tac (simpset()) state
+
+(*For harder protocols (such as Recur) where we have to set up some
+ nonces and keys initially*)
+fun basic_possibility_tac st = st |>
+ REPEAT
+ (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ THEN
+ REPEAT_FIRST (resolve_tac [refl, conjI]))
*}
method_setup possibility = {*
@@ -394,22 +437,4 @@
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
"for proving possibility theorems"
-
-
-lemmas analz_image_freshK_simps =
- simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
- disj_comms
- image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
- analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
- insert_Key_singleton
- Key_not_used insert_Key_image Un_assoc [THEN sym]
-
-ML
-{*
-val analz_image_freshK_ss =
- simpset() delsimps [image_insert, image_Un]
- delsimps [imp_disjL] (*reduces blow-up*)
- addsimps thms"analz_image_freshK_simps"
-*}
-
end
--- a/src/HOL/Auth/Recur.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Recur.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,11 +2,11 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-Inductive relation "recur" for the Recursive Authentication protocol.
*)
-theory Recur = Shared:
+header{*The Otway-Bull Recursive Authentication Protocol*}
+
+theory Recur = Public:
text{*End marker for message bundles*}
syntax END :: "msg"
@@ -63,26 +63,26 @@
(*Alice initiates a protocol run.
END is a placeholder to terminate the nesting.*)
- RA1: "[| evs1: recur; Nonce NA \<notin> used evs1 |]
+ RA1: "[| evs1 \<in> recur; Nonce NA \<notin> used evs1 |]
==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
# evs1 \<in> recur"
(*Bob's response to Alice's message. C might be the Server.
We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
it complicates proofs, so B may respond to any message at all!*)
- RA2: "[| evs2: recur; Nonce NB \<notin> used evs2;
+ RA2: "[| evs2 \<in> recur; Nonce NB \<notin> used evs2;
Says A' B PA \<in> set evs2 |]
==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
# evs2 \<in> recur"
(*The Server receives Bob's message and prepares a response.*)
- RA3: "[| evs3: recur; Says B' Server PB \<in> set evs3;
+ RA3: "[| evs3 \<in> recur; Says B' Server PB \<in> set evs3;
(PB,RB,K) \<in> respond evs3 |]
==> Says Server B RB # evs3 \<in> recur"
(*Bob receives the returned message and compares the Nonces with
those in the message he previously sent the Server.*)
- RA4: "[| evs4: recur;
+ RA4: "[| evs4 \<in> recur;
Says B C {|XH, Agent B, Agent C, Nonce NB,
XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
@@ -98,7 +98,7 @@
the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts,
etc.
- Oops: "[| evso: recur; Says Server B RB \<in> set evso;
+ Oops: "[| evso \<in> recur; Says Server B RB \<in> set evso;
RB \<in> responses evs'; Key K \<in> parts {RB} |]
==> Notes Spy {|Key K, RB|} # evso \<in> recur"
*)
@@ -129,28 +129,30 @@
text{*Case two: Alice, Bob and the server*}
-lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K' |]
- ==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
+lemma "[| Key K \<notin> used []; Key K' \<notin> used []; K \<noteq> K';
+ Nonce NA \<notin> used []; Nonce NB \<notin> used []; NA < NB |]
+ ==> \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-apply (cut_tac Nonce_supply2, clarify)
apply (intro exI bexI)
apply (rule_tac [2]
- recur.Nil [THEN recur.RA1,
- THEN recur.RA2,
- THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
- THEN recur.RA4])
-apply possibility
+ recur.Nil
+ [THEN recur.RA1 [of _ NA],
+ THEN recur.RA2 [of _ NB],
+ THEN recur.RA3 [OF _ _ respond.One
+ [THEN respond.Cons [of _ _ K _ K']]],
+ THEN recur.RA4], possibility)
apply (auto simp add: used_Cons)
done
(*Case three: Alice, Bob, Charlie and the server Rather slow (5 seconds)*)
lemma "[| Key K \<notin> used []; Key K' \<notin> used [];
- Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'' |]
+ Key K'' \<notin> used []; K \<noteq> K'; K' \<noteq> K''; K \<noteq> K'';
+ Nonce NA \<notin> used []; Nonce NB \<notin> used []; Nonce NC \<notin> used [];
+ NA < NB; NB < NC |]
==> \<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-apply (cut_tac Nonce_supply3, clarify)
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil [THEN recur.RA1,
@@ -163,7 +165,6 @@
apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
done
-(**** Inductive proofs about recur ****)
lemma respond_imp_not_used: "(PA,RB,KAB) \<in> respond evs ==> Key KAB \<notin> used evs"
by (erule respond.induct, simp_all)
@@ -236,12 +237,13 @@
==> \<forall>K KK. KK \<subseteq> - (range shrK) -->
(Key K \<in> analz (insert RB (Key`KK Un H))) =
(K \<in> KK | Key K \<in> analz (insert RB H))"
-by (erule responses.induct,
- simp_all del: image_insert
- add: analz_image_freshK_simps)
+apply (erule responses.induct)
+apply (simp_all del: image_insert
+ add: analz_image_freshK_simps, auto)
+done
-text{*Version for the protocol. Proof is almost trivial, thanks to the lemma.*}
+text{*Version for the protocol. Proof is easy, thanks to the lemma.*}
lemma raw_analz_image_freshK:
"evs \<in> recur ==>
\<forall>K KK. KK \<subseteq> - (range shrK) -->
@@ -320,9 +322,10 @@
lemma shrK_in_analz_respond [simp]:
"[| RB \<in> responses evs; evs \<in> recur |]
==> (Key (shrK B) \<in> analz (insert RB (spies evs))) = (B:bad)"
-by (erule responses.induct,
- simp_all del: image_insert
- add: analz_image_freshK_simps resp_analz_image_freshK)
+apply (erule responses.induct)
+apply (simp_all del: image_insert
+ add: analz_image_freshK_simps resp_analz_image_freshK, auto)
+done
lemma resp_analz_insert_lemma:
@@ -452,8 +455,6 @@
drule_tac [6] RA4_parts_spies,
drule_tac [4] RA2_parts_spies,
simp_all)
-txt{*Nil*}
-apply force
txt{*Fake, RA3*}
apply (blast dest: Hash_in_parts_respond)+
done
--- a/src/HOL/Auth/WooLam.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/WooLam.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,19 +2,21 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-Inductive relation "woolam" for the Woo-Lam protocol.
-
-Simplified version from page 11 of
- Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols.
- IEEE Trans. S.E. 22(1), 1996, pages 6-15.
-
-Note: this differs from the Woo-Lam protocol discussed by Lowe in his paper
- Some New Attacks upon Security Protocols.
- Computer Security Foundations Workshop, 1996.
*)
-theory WooLam = Shared:
+header{*The Woo-Lam Protocol*}
+
+theory WooLam = Public:
+
+text{*Simplified version from page 11 of
+ Abadi and Needham (1996).
+ Prudent Engineering Practice for Cryptographic Protocols.
+ IEEE Trans. S.E. 22(1), pages 6-15.
+
+Note: this differs from the Woo-Lam protocol discussed by Lowe (1996):
+ Some New Attacks upon Security Protocols.
+ Computer Security Foundations Workshop
+*}
consts woolam :: "event list set"
inductive woolam
@@ -87,8 +89,7 @@
(*Spy never sees a good agent's shared key!*)
lemma Spy_see_shrK [simp]:
"evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule woolam.induct, force, simp_all, blast+)
-done
+by (erule woolam.induct, force, simp_all, blast+)
lemma Spy_analz_shrK [simp]:
"evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
@@ -108,8 +109,7 @@
"[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
A \<notin> bad; evs \<in> woolam |]
==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
-done
+by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
(*Guarantee for Server: if it gets a message containing a certificate from
Alice, then she originated that certificate. But we DO NOT know that B
@@ -130,16 +130,14 @@
evs \<in> woolam |]
==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
\<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
-done
+by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
(*If the encrypted message appears then it originated with the Server!*)
lemma NB_Crypt_imp_Server_msg [rule_format]:
"[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
B \<notin> bad; evs \<in> woolam |]
==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
-done
+by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
(*Guarantee for B. If B gets the Server's certificate then A has encrypted
the nonce using her key. This event can be no older than the nonce itself.
@@ -156,8 +154,7 @@
lemma B_said_WL2:
"[| Says B A (Nonce NB) \<in> set evs; B \<noteq> Spy; evs \<in> woolam |]
==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
-done
+by (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
(**CANNOT be proved because A doesn't know where challenges come from...*)
--- a/src/HOL/Auth/Yahalom.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,19 +2,18 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-Inductive relation "yahalom" for the Yahalom protocol.
-
-From page 257 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-
-This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
*)
header{*The Yahalom Protocol*}
-theory Yahalom = Shared:
+theory Yahalom = Public:
+
+text{*From page 257 of
+ Burrows, Abadi and Needham (1989). A Logic of Authentication.
+ Proc. Royal Soc. 426
+
+This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
+*}
consts yahalom :: "event list set"
inductive "yahalom"
@@ -46,7 +45,7 @@
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
+ YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys;
Gets Server
{|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
\<in> set evs3 |]
@@ -55,10 +54,12 @@
Crypt (shrK B) {|Agent A, Key KAB|}|}
# evs3 \<in> yahalom"
- (*Alice receives the Server's (?) message, checks her Nonce, and
+ YM4:
+ --{*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce. The premise
- A \<noteq> Server is needed to prove Says_Server_not_range.*)
- YM4: "[| evs4 \<in> yahalom; A \<noteq> Server;
+ @{term "A \<noteq> Server"} is needed for @{text Says_Server_not_range}.
+ Alice can check that K is symmetric by its length.*}
+ "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys;
Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
\<in> set evs4;
Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
@@ -87,24 +88,27 @@
declare Fake_parts_insert_in_Un [dest]
declare analz_into_parts [dest]
-(*A "possibility property": there are traces that reach the end*)
-lemma "[| A \<noteq> Server; Key K \<notin> used [] |]
- ==> \<exists>X NB. \<exists>evs \<in> yahalom.
+text{*A "possibility property": there are traces that reach the end*}
+lemma "[| A \<noteq> Server; K \<in> symKeys; Key K \<notin> used [] |]
+ ==> \<exists>X NB. \<exists>evs \<in> yahalom.
Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] yahalom.Nil
- [THEN yahalom.YM1, THEN yahalom.Reception,
- THEN yahalom.YM2, THEN yahalom.Reception,
- THEN yahalom.YM3, THEN yahalom.Reception,
+ [THEN yahalom.YM1, THEN yahalom.Reception,
+ THEN yahalom.YM2, THEN yahalom.Reception,
+ THEN yahalom.YM3, THEN yahalom.Reception,
THEN yahalom.YM4])
-apply (possibility, simp add: used_Cons)
+apply (possibility, simp add: used_Cons)
done
+
+subsection{*Regularity Lemmas for Yahalom*}
+
lemma Gets_imp_Says:
"[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
by (erule rev_mp, erule yahalom.induct, auto)
-(*Must be proved separately for each protocol*)
+text{*Must be proved separately for each protocol*}
lemma Gets_imp_knows_Spy:
"[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> X \<in> knows Spy evs"
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
@@ -112,33 +116,30 @@
declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
-(**** Inductive proofs about yahalom ****)
-
-(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+text{*Lets us treat YM4 using a similar argument as for the Fake case.*}
lemma YM4_analz_knows_Spy:
- "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
+ "[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
==> X \<in> analz (knows Spy evs)"
by blast
-lemmas YM4_parts_knows_Spy =
+lemmas YM4_parts_knows_Spy =
YM4_analz_knows_Spy [THEN analz_into_parts, standard]
-(*For Oops*)
+text{*For Oops*}
lemma YM4_Key_parts_knows_Spy:
- "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
+ "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \<in> set evs
==> K \<in> parts (knows Spy evs)"
by (blast dest!: parts.Body Says_imp_knows_Spy [THEN parts.Inj])
-(** 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 (knows Spy 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> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
-apply (erule yahalom.induct, force,
- drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
-done
+by (erule yahalom.induct, force,
+ drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
lemma Spy_analz_shrK [simp]:
"evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
@@ -148,39 +149,37 @@
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad"
by (blast dest: Spy_see_shrK)
-(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-lemma new_keys_not_used [rule_format, simp]:
- "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
-apply (erule yahalom.induct, force,
+text{*Nobody can have used non-existent keys!
+ Needed to apply @{text analz_insert_Key}*}
+lemma new_keys_not_used [simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
+ ==> K \<notin> keysFor (parts (spies evs))"
+apply (erule rev_mp)
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
txt{*Fake*}
-apply (force dest!: keysFor_parts_insert)
-txt{*YM3, YM4*}
-apply blast+
+apply (force dest!: keysFor_parts_insert, auto)
done
-(*Earlier, all protocol proofs declared this theorem.
- But only a few proofs need it, e.g. Yahalom and Kerberos IV.*)
+text{*Earlier, all protocol proofs declared this theorem.
+ But only a few proofs need it, e.g. Yahalom and Kerberos IV.*}
lemma new_keys_not_analzd:
- "[|evs \<in> yahalom; Key K \<notin> used evs|] ==> K \<notin> keysFor (analz (knows Spy evs))"
-by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
+ "[|K \<in> symKeys; evs \<in> yahalom; Key K \<notin> used evs|]
+ ==> K \<notin> keysFor (analz (knows Spy evs))"
+by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD])
-(*Describes the form of K when the Server sends this message. Useful for
- Oops as well as main secrecy property.*)
+text{*Describes the form of K when the Server sends this message. Useful for
+ Oops as well as main secrecy property.*}
lemma Says_Server_not_range [simp]:
- "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
- \<in> set evs; evs \<in> yahalom |]
+ "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
+ \<in> set evs; evs \<in> yahalom |]
==> K \<notin> range shrK"
-apply (erule rev_mp, erule yahalom.induct, simp_all, blast)
-done
+by (erule rev_mp, erule yahalom.induct, simp_all, blast)
-(*For proofs involving analz.
-val analz_knows_Spy_tac =
- ftac YM4_analz_knows_Spy 7 THEN assume_tac 7
-*)
+subsection{*Secrecy Theorems*}
(****
The following is to prove theorems of the form
@@ -191,412 +190,415 @@
A more general formula must be proved inductively.
****)
-(** Session keys are not used to encrypt other session keys **)
+text{* Session keys are not used to encrypt other session keys *}
lemma analz_image_freshK [rule_format]:
- "evs \<in> yahalom ==>
- \<forall>K KK. KK <= - (range shrK) -->
- (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
+ "evs \<in> yahalom ==>
+ \<forall>K KK. KK <= - (range shrK) -->
+ (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
-apply (erule yahalom.induct, force,
- drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
+apply (erule yahalom.induct,
+ drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
apply (simp only: Says_Server_not_range analz_image_freshK_simps)
done
lemma analz_insert_freshK:
- "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
+ "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
(K = KAB | Key K \<in> analz (knows Spy evs))"
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 A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
- Says Server A'
- {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
- evs \<in> yahalom |]
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
+ Says Server A'
+ {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|} \<in> set evs;
+ evs \<in> yahalom |]
==> A=A' & B=B' & na=na' & nb=nb'"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, simp_all)
-(*YM3, by freshness, and YM4*)
+txt{*YM3, by freshness, and YM4*}
apply blast+
done
-(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-
+text{*Crucial secrecy property: Spy does not see the keys sent in msg YM3*}
lemma secrecy_lemma:
- "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
- \<in> set evs -->
- Notes Spy {|na, nb, Key K|} \<notin> set evs -->
+ "[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs -->
+ Notes Spy {|na, nb, Key K|} \<notin> set evs -->
Key K \<notin> analz (knows Spy evs)"
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*)
-apply (blast dest: unique_session_keys)+ (*YM3, Oops*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) --{*Fake*}
+apply (blast dest: unique_session_keys)+ --{*YM3, Oops*}
done
-(*Final version*)
+text{*Final version*}
lemma Spy_not_see_encrypted_key:
- "[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
- \<in> set evs;
- Notes Spy {|na, nb, Key K|} \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
+ \<in> set evs;
+ Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: secrecy_lemma)
-(** Security Guarantee for A upon receiving YM3 **)
+subsubsection{* Security Guarantee for A upon receiving YM3 *}
-(*If the encrypted message appears then it originated with the Server*)
+text{*If the encrypted message appears then it originated with the Server*}
lemma A_trusts_YM3:
- "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
- A \<notin> bad; evs \<in> yahalom |]
- ==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ A \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, nb|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
\<in> set evs"
apply (erule rev_mp)
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3*)
+txt{*Fake, YM3*}
apply blast+
done
-(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text A_trusts_YM3} with
+ @{text Spy_not_see_encrypted_key}*}
lemma A_gets_good_key:
- "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
- Notes Spy {|na, nb, Key K|} \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
+ Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
-(** Security Guarantees for B upon receiving YM4 **)
+
+subsubsection{* Security Guarantees for B upon receiving YM4 *}
-(*B knows, by the first part of A's message, that the Server distributed
- the key for A and B. But this part says nothing about nonces.*)
+text{*B knows, by the first part of A's message, that the Server distributed
+ the key for A and B. But this part says nothing about nonces.*}
lemma B_trusts_YM4_shrK:
- "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
- B \<notin> bad; evs \<in> yahalom |]
- ==> \<exists>NA NB. Says Server A
- {|Crypt (shrK A) {|Agent B, Key K,
- Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ "[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
+ B \<notin> bad; evs \<in> yahalom |]
+ ==> \<exists>NA NB. Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K,
+ Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
\<in> set evs"
apply (erule rev_mp)
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3*)
+txt{*Fake, YM3*}
apply blast+
done
-(*B knows, by the second part of A's message, that the Server distributed
- the key quoting nonce NB. This part says nothing about agent names.
+text{*B knows, by the second part of A's message, that the Server distributed
+ the key quoting nonce NB. This part says nothing about agent names.
Secrecy of NB is crucial. Note that Nonce NB \<notin> analz(knows Spy evs) must
- be the FIRST antecedent of the induction formula.*)
-lemma B_trusts_YM4_newK[rule_format]:
+ be the FIRST antecedent of the induction formula.*}
+lemma B_trusts_YM4_newK [rule_format]:
"[|Crypt K (Nonce NB) \<in> parts (knows Spy evs);
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
- ==> \<exists>A B NA. Says Server A
+ ==> \<exists>A B NA. Says Server A
{|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ Crypt (shrK B) {|Agent A, Key K|}|}
\<in> set evs"
apply (erule rev_mp, erule rev_mp)
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
-(*Fake, YM3*)
+txt{*Fake, YM3*}
apply blast
apply blast
-(*YM4*)
-(*A is uncompromised because NB is secure
- A's certificate guarantees the existence of the Server message*)
-apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
- dest: Says_imp_spies
+txt{*YM4. A is uncompromised because NB is secure
+ A's certificate guarantees the existence of the Server message*}
+apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
+ dest: Says_imp_spies
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
done
-(**** Towards proving secrecy of Nonce NB ****)
+subsubsection{* Towards proving secrecy of Nonce NB *}
-(** Lemmas about the predicate KeyWithNonce **)
+text{*Lemmas about the predicate KeyWithNonce*}
-lemma KeyWithNonceI:
- "Says Server A
- {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
+lemma KeyWithNonceI:
+ "Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}
\<in> set evs ==> KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast)
-lemma KeyWithNonce_Says [simp]:
- "KeyWithNonce K NB (Says S A X # evs) =
+lemma KeyWithNonce_Says [simp]:
+ "KeyWithNonce K NB (Says S A X # evs) =
(Server = S &
- (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
+ (\<exists>B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|})
| KeyWithNonce K NB evs)"
by (simp add: KeyWithNonce_def, blast)
-lemma KeyWithNonce_Notes [simp]:
+lemma KeyWithNonce_Notes [simp]:
"KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs"
by (simp add: KeyWithNonce_def)
-lemma KeyWithNonce_Gets [simp]:
+lemma KeyWithNonce_Gets [simp]:
"KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs"
by (simp add: KeyWithNonce_def)
-(*A fresh key cannot be associated with any nonce
- (with respect to a given trace). *)
-lemma fresh_not_KeyWithNonce:
- "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs"
+text{*A fresh key cannot be associated with any nonce
+ (with respect to a given trace). *}
+lemma fresh_not_KeyWithNonce:
+ "Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast)
-(*The Server message associates K with NB' and therefore not with any
- other nonce NB.*)
-lemma Says_Server_KeyWithNonce:
- "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
- \<in> set evs;
- NB \<noteq> NB'; evs \<in> yahalom |]
+text{*The Server message associates K with NB' and therefore not with any
+ other nonce NB.*}
+lemma Says_Server_KeyWithNonce:
+ "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|}
+ \<in> set evs;
+ NB \<noteq> NB'; evs \<in> yahalom |]
==> ~ KeyWithNonce K NB evs"
by (unfold KeyWithNonce_def, blast dest: unique_session_keys)
-(*The only nonces that can be found with the help of session keys are
+text{*The only nonces that can be found with the help of session keys are
those distributed as nonce NB by the Server. The form of the theorem
- recalls analz_image_freshK, but it is much more complicated.*)
+ recalls @{text analz_image_freshK}, but it is much more complicated.*}
-(*As with analz_image_freshK, we take some pains to express the property
- as a logical equivalence so that the simplifier can apply it.*)
+text{*As with @{text analz_image_freshK}, we take some pains to express the
+ property as a logical equivalence so that the simplifier can apply it.*}
lemma Nonce_secrecy_lemma:
- "P --> (X \<in> analz (G Un H)) --> (X \<in> analz H) ==>
+ "P --> (X \<in> analz (G Un H)) --> (X \<in> analz H) ==>
P --> (X \<in> analz (G Un H)) = (X \<in> analz H)"
by (blast intro: analz_mono [THEN subsetD])
lemma Nonce_secrecy:
- "evs \<in> yahalom ==>
- (\<forall>KK. KK <= - (range shrK) -->
- (\<forall>K \<in> KK. ~ KeyWithNonce K NB evs) -->
- (Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) =
+ "evs \<in> yahalom ==>
+ (\<forall>KK. KK <= - (range shrK) -->
+ (\<forall>K \<in> KK. K \<in> symKeys --> ~ KeyWithNonce K NB evs) -->
+ (Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) =
(Nonce NB \<in> analz (knows Spy evs)))"
-apply (erule yahalom.induct, force,
- frule_tac [6] YM4_analz_knows_Spy)
+apply (erule yahalom.induct,
+ frule_tac [7] YM4_analz_knows_Spy)
apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI])
-apply (simp_all del: image_insert image_Un
+apply (simp_all del: image_insert image_Un
add: analz_image_freshK_simps split_ifs
- all_conj_distrib ball_conj_distrib
+ all_conj_distrib ball_conj_distrib
analz_image_freshK fresh_not_KeyWithNonce
imp_disj_not1 (*Moves NBa\<noteq>NB to the front*)
Says_Server_KeyWithNonce)
-(*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce,
+txt{*For Oops, simplification proves NBa\<noteq>NB. By Says_Server_KeyWithNonce,
we get (~ KeyWithNonce K NB evs); then simplification can apply the
- induction hypothesis with KK = {K}.*)
-(*Fake*)
+ induction hypothesis with KK = {K}.*}
+txt{*Fake*}
apply spy_analz
-(*YM4*) (** LEVEL 6 **)
+txt{*YM2*}
+apply blast
+txt{*YM3*}
+apply blast
+txt{*YM4*}
apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
-(*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps make
- the next step faster.*)
+txt{*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps
+ make the next step faster.*}
apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
dest: analz.Inj
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3, THEN KeyWithNonceI])
done
-(*Version required below: if NB can be decrypted using a session key then it
- was distributed with that key. The more general form above is required
- for the induction to carry through.*)
+text{*Version required below: if NB can be decrypted using a session key then
+ it was distributed with that key. The more general form above is required
+ for the induction to carry through.*}
lemma single_Nonce_secrecy:
- "[| Says Server A
- {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
- \<in> set evs;
- NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |]
- ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
+ "[| Says Server A
+ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}
+ \<in> set evs;
+ NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom |]
+ ==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) =
(Nonce NB \<in> analz (knows Spy evs))"
by (simp_all del: image_insert image_Un imp_disjL
add: analz_image_freshK_simps split_ifs
Nonce_secrecy Says_Server_KeyWithNonce)
-(*** The Nonce NB uniquely identifies B's message. ***)
+subsubsection{* The Nonce NB uniquely identifies B's message. *}
lemma unique_NB:
- "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
- Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
- evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |]
+ "[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
+ Crypt (shrK B') {|Agent A', Nonce NA', nb|} \<in> parts (knows Spy evs);
+ evs \<in> yahalom; B \<notin> bad; B' \<notin> bad |]
==> NA' = NA & A' = A & B' = B"
apply (erule rev_mp, erule rev_mp)
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, and YM2 by freshness*)
+txt{*Fake, and YM2 by freshness*}
apply blast+
done
-(*Variant useful for proving secrecy of NB. Because nb is assumed to be
- secret, we no longer must assume B, B' not bad.*)
+text{*Variant useful for proving secrecy of NB. Because nb is assumed to be
+ secret, we no longer must assume B, B' not bad.*}
lemma Says_unique_NB:
- "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
- \<in> set evs;
- Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
- \<in> set evs;
- nb \<notin> analz (knows Spy evs); evs \<in> yahalom |]
+ "[| Says C S {|X, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ \<in> set evs;
+ Gets S' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|}
+ \<in> set evs;
+ nb \<notin> analz (knows Spy evs); evs \<in> yahalom |]
==> NA' = NA & A' = A & B' = B"
-by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
+by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
dest: Says_imp_spies unique_NB parts.Inj analz.Inj)
-(** A nonce value is never used both as NA and as NB **)
+subsubsection{* A nonce value is never used both as NA and as NB *}
lemma no_nonce_YM1_YM2:
"[|Crypt (shrK B') {|Agent A', Nonce NB, nb'|} \<in> parts(knows Spy evs);
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom|]
==> Crypt (shrK B) {|Agent A, na, Nonce NB|} \<notin> parts(knows Spy evs)"
apply (erule rev_mp, erule rev_mp)
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
-(*Fake, YM2*)
+txt{*Fake, YM2*}
apply blast+
done
-(*The Server sends YM3 only in response to YM2.*)
+text{*The Server sends YM3 only in response to YM2.*}
lemma Says_Server_imp_YM2:
"[| Says Server A {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} \<in> set evs;
- evs \<in> yahalom |]
- ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
+ evs \<in> yahalom |]
+ ==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
\<in> set evs"
-apply (erule rev_mp, erule yahalom.induct, auto)
-done
+by (erule rev_mp, erule yahalom.induct, auto)
-
-(*A vital theorem for B, that nonce NB remains secure from the Spy.*)
+text{*A vital theorem for B, that nonce NB remains secure from the Spy.*}
lemma Spy_not_see_NB :
- "[| Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ "[| Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
\<in> set evs;
(\<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Nonce NB \<notin> analz (knows Spy evs)"
apply (erule rev_mp, erule rev_mp)
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_analz_knows_Spy)
apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
analz_insert_freshK)
-(*Fake*)
+txt{*Fake*}
apply spy_analz
-(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
+txt{*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*}
apply blast
-(*YM2*)
+txt{*YM2*}
apply blast
-(*Prove YM3 by showing that no NB can also be an NA*)
+txt{*Prove YM3 by showing that no NB can also be an NA*}
apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
-(** LEVEL 7: YM4 and Oops remain **)
+txt{*LEVEL 7: YM4 and Oops remain*}
apply (clarify, simp add: all_conj_distrib)
-(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*)
-(*Case analysis on Aa:bad; PROOF FAILED problems
- use Says_unique_NB to identify message components: Aa=A, Ba=B*)
-apply (blast dest!: Says_unique_NB
- parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
+txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*}
+txt{*Case analysis on Aa:bad; PROOF FAILED problems
+ use Says_unique_NB to identify message components: Aa=A, Ba=B*}
+apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
+ parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]
dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
Spy_not_see_encrypted_key)
-(*Oops case: if the nonce is betrayed now, show that the Oops event is
- covered by the quantified Oops assumption.*)
+txt{*Oops case: if the nonce is betrayed now, show that the Oops event is
+ covered by the quantified Oops assumption.*}
apply (clarify, simp add: all_conj_distrib)
apply (frule Says_Server_imp_YM2, assumption)
apply (case_tac "NB = NBa")
-(*If NB=NBa then all other components of the Oops message agree*)
+txt{*If NB=NBa then all other components of the Oops message agree*}
apply (blast dest: Says_unique_NB)
-(*case NB \<noteq> NBa*)
+txt{*case NB \<noteq> NBa*}
apply (simp add: single_Nonce_secrecy)
apply (blast dest!: no_nonce_YM1_YM2 (*to prove NB\<noteq>NAa*))
done
-(*B's session key guarantee from YM4. The two certificates contribute to a
+text{*B's session key guarantee from YM4. The two certificates contribute to a
single conclusion about the Server's message. Note that the "Notes Spy"
assumption must quantify over \<forall>POSSIBLE keys instead of our particular K.
If this run is broken and the spy substitutes a certificate containing an
- old key, B has no means of telling.*)
+ old key, B has no means of telling.*}
lemma B_trusts_YM4:
- "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
- Crypt K (Nonce NB)|} \<in> set evs;
- Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- \<in> set evs;
- \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> Says Server A
- {|Crypt (shrK A) {|Agent B, Key K,
- Nonce NA, Nonce NB|},
- Crypt (shrK B) {|Agent A, Key K|}|}
+ "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
+ Crypt K (Nonce NB)|} \<in> set evs;
+ Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<in> set evs;
+ \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says Server A
+ {|Crypt (shrK A) {|Agent B, Key K,
+ Nonce NA, Nonce NB|},
+ Crypt (shrK B) {|Agent A, Key K|}|}
\<in> set evs"
-by (blast dest: Spy_not_see_NB Says_unique_NB
+by (blast dest: Spy_not_see_NB Says_unique_NB
Says_Server_imp_YM2 B_trusts_YM4_newK)
-(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text B_trusts_YM4} with
+ @{text Spy_not_see_encrypted_key}*}
lemma B_gets_good_key:
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
Crypt K (Nonce NB)|} \<in> set evs;
- Says B Server
- {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
- \<in> set evs;
- \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ Says B Server
+ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
+ \<in> set evs;
+ \<forall>k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key)
-(*** Authenticating B to A ***)
+subsection{*Authenticating B to A*}
-(*The encryption in message YM2 tells us it cannot be faked.*)
+text{*The encryption in message YM2 tells us it cannot be faked.*}
lemma B_Said_YM2 [rule_format]:
"[|Crypt (shrK B) {|Agent A, Nonce NA, nb|} \<in> parts (knows Spy evs);
evs \<in> yahalom|]
==> B \<notin> bad -->
Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
\<in> set evs"
-apply (erule rev_mp, erule yahalom.induct, force,
+apply (erule rev_mp, erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
done
-(*If the server sends YM3 then B sent YM2*)
+text{*If the server sends YM3 then B sent YM2*}
lemma YM3_auth_B_to_A_lemma:
- "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+ "[|Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
\<in> set evs; evs \<in> yahalom|]
- ==> B \<notin> bad -->
+ ==> B \<notin> bad -->
Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
\<in> set evs"
apply (erule rev_mp, erule yahalom.induct, simp_all)
-(*YM3, YM4*)
+txt{*YM3, YM4*}
apply (blast dest!: B_Said_YM2)+
done
-(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
+text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
lemma YM3_auth_B_to_A:
- "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
- \<in> set evs;
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
- ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
+ "[| Gets A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|}
+ \<in> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}
\<in> set evs"
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma elim: knows_Spy_partsEs)
-(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
+subsection{*Authenticating A to B using the certificate
+ @{term "Crypt K (Nonce NB)"}*}
-(*Assuming the session key is secure, if both certificates are present then
+text{*Assuming the session key is secure, if both certificates are present then
A has said NB. We can't be sure about the rest of A's message, but only
- NB matters for freshness.*)
+ NB matters for freshness.*}
lemma A_Said_YM3_lemma [rule_format]:
"evs \<in> yahalom
==> Key K \<notin> analz (knows Spy evs) -->
@@ -604,24 +606,26 @@
Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs) -->
B \<notin> bad -->
(\<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs)"
-apply (erule yahalom.induct, force,
+apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
-(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
+txt{*YM3: by @{text new_keys_not_used}, the message
+ @{term "Crypt K (Nonce NB)"} could not exist*}
apply (force dest!: Crypt_imp_keysFor)
-(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
+txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
+ If not, use the induction hypothesis*}
apply (simp add: ex_disj_distrib)
-(*yes: apply unicity of session keys*)
+txt{*yes: apply unicity of session keys*}
apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
- Crypt_Spy_analz_bad
+ Crypt_Spy_analz_bad
dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
done
-(*If B receives YM4 then A has used nonce NB (and therefore is alive).
+text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
Moreover, A associates K with NB (thus is talking about the same run).
- Other premises guarantee secrecy of K.*)
+ Other premises guarantee secrecy of K.*}
lemma YM4_imp_A_Said_YM3 [rule_format]:
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
Crypt K (Nonce NB)|} \<in> set evs;
@@ -631,7 +635,7 @@
(\<forall>NA k. Notes Spy {|Nonce NA, Nonce NB, k|} \<notin> set evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
-by (blast intro!: A_Said_YM3_lemma
+by (blast intro!: A_Said_YM3_lemma
dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
end
--- a/src/HOL/Auth/Yahalom2.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,18 +2,22 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
+*)
+header{*The Yahalom Protocol, Variant 2*}
+
+theory Yahalom2 = Public:
+
+text{*
This version trades encryption of NB for additional explicitness in YM3.
Also in YM3, care is taken to make the two certificates distinct.
From page 259 of
- Burrows, Abadi and Needham. A Logic of Authentication.
- Proc. Royal Soc. 426 (1989)
-*)
+ Burrows, Abadi and Needham (1989). A Logic of Authentication.
+ Proc. Royal Soc. 426
-header{*The Yahalom Protocol, Variant 2*}
-
-theory Yahalom2 = Shared:
+This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
+*}
consts yahalom :: "event list set"
inductive "yahalom"
@@ -89,7 +93,7 @@
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
THEN yahalom.YM4])
-apply (possibility, simp add: used_Cons)
+apply (possibility, simp add: used_Cons)
done
lemma Gets_imp_Says:
@@ -134,20 +138,26 @@
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad"
by (blast dest: Spy_see_shrK)
-(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-lemma new_keys_not_used [rule_format, simp]:
- "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
+text{*Nobody can have used non-existent keys!
+ Needed to apply @{text analz_insert_Key}*}
+lemma new_keys_not_used [simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
+ ==> K \<notin> keysFor (parts (spies evs))"
+apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
txt{*Fake*}
apply (force dest!: keysFor_parts_insert)
-txt{*YM3, YM4*}
-apply blast+
+txt{*YM3*}
+apply blast
+txt{*YM4*}
+apply auto
+apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj])
done
-(*Describes the form of K when the Server sends this message. Useful for
- Oops as well as main secrecy property.*)
+text{*Describes the form of K when the Server sends this message. Useful for
+ Oops as well as main secrecy property.*}
lemma Says_Server_message_form:
"[| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|}
\<in> set evs; evs \<in> yahalom |]
@@ -171,8 +181,9 @@
\<forall>K KK. KK <= - (range shrK) -->
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
-apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
- drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
+apply (erule yahalom.induct)
+apply (frule_tac [8] Says_Server_message_form)
+apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
done
lemma analz_insert_freshK:
@@ -214,7 +225,7 @@
done
-(*Final version*)
+text{*Final version*}
lemma Spy_not_see_encrypted_key:
"[| Says Server A
{|nb, Crypt (shrK A) {|Agent B, Key K, na|},
@@ -227,12 +238,12 @@
-text{*This form is an immediate consequence of the previous result. It is
+text{*This form is an immediate consequence of the previous result. It is
similar to the assertions established by other methods. It is equivalent
to the previous result in that the Spy already has @{term analz} and
-@{term synth} at his disposal. However, the conclusion
+@{term synth} at his disposal. However, the conclusion
@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
-other than Fake are trivial, while Fake requires
+other than Fake are trivial, while Fake requires
@{term "Key K \<notin> analz (knows Spy evs)"}. *}
lemma Spy_not_know_encrypted_key:
"[| Says Server A
@@ -247,8 +258,8 @@
subsection{*Security Guarantee for A upon receiving YM3*}
-(*If the encrypted message appears then it originated with the Server.
- May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
+text{*If the encrypted message appears then it originated with the Server.
+ May now apply @{text Spy_not_see_encrypted_key}, subject to its conditions.*}
lemma A_trusts_YM3:
"[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> yahalom |]
@@ -263,7 +274,8 @@
apply blast+
done
-(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text A_trusts_YM3} with
+@{text Spy_not_see_encrypted_key}*}
theorem A_gets_good_key:
"[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> parts (knows Spy evs);
\<forall>nb. Notes Spy {|na, nb, Key K|} \<notin> set evs;
@@ -274,8 +286,8 @@
subsection{*Security Guarantee for B upon receiving YM4*}
-(*B knows, by the first part of A's message, that the Server distributed
- the key for A and B, and has associated it with NB.*)
+text{*B knows, by the first part of A's message, that the Server distributed
+ the key for A and B, and has associated it with NB.*}
lemma B_trusts_YM4_shrK:
"[| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
\<in> parts (knows Spy evs);
@@ -288,16 +300,16 @@
apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3*)
+txt{*Fake, YM3*}
apply blast+
done
-(*With this protocol variant, we don't need the 2nd part of YM4 at all:
- Nonce NB is available in the first part.*)
+text{*With this protocol variant, we don't need the 2nd part of YM4 at all:
+ Nonce NB is available in the first part.*}
-(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
- because we do not have to show that NB is secret. *)
+text{*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom
+ because we do not have to show that NB is secret. *}
lemma B_trusts_YM4:
"[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
\<in> set evs;
@@ -310,7 +322,8 @@
by (blast dest!: B_trusts_YM4_shrK)
-(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text B_trusts_YM4} with
+@{text Spy_not_see_encrypted_key}*}
theorem B_gets_good_key:
"[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
\<in> set evs;
@@ -322,7 +335,7 @@
subsection{*Authenticating B to A*}
-(*The encryption in message YM2 tells us it cannot be faked.*)
+text{*The encryption in message YM2 tells us it cannot be faked.*}
lemma B_Said_YM2:
"[| Crypt (shrK B) {|Agent A, Nonce NA|} \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> yahalom |]
@@ -332,12 +345,12 @@
apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM2*)
+txt{*Fake, YM2*}
apply blast+
done
-(*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
+text{*If the server sends YM3 then B sent YM2, perhaps with a different NB*}
lemma YM3_auth_B_to_A_lemma:
"[| Says Server A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
\<in> set evs;
@@ -347,7 +360,7 @@
\<in> set evs"
apply (erule rev_mp)
apply (erule yahalom.induct, simp_all)
-(*Fake, YM2, YM3*)
+txt{*Fake, YM2, YM3*}
apply (blast dest!: B_Said_YM2)+
done
@@ -366,13 +379,13 @@
text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
-(*Assuming the session key is secure, if both certificates are present then
+text{*Assuming the session key is secure, if both certificates are present then
A has said NB. We can't be sure about the rest of A's message, but only
- NB matters for freshness. Note that Key K \<notin> analz (knows Spy evs) must be
- the FIRST antecedent of the induction formula.*)
+ NB matters for freshness. Note that @{term "Key K \<notin> analz (knows Spy evs)"}
+ must be the FIRST antecedent of the induction formula.*}
-(*This lemma allows a use of unique_session_keys in the next proof,
- which otherwise is extremely slow.*)
+text{*This lemma allows a use of @{text unique_session_keys} in the next proof,
+ which otherwise is extremely slow.*}
lemma secure_unique_session_keys:
"[| Crypt (shrK A) {|Agent B, Key K, na|} \<in> analz (spies evs);
Crypt (shrK A') {|Agent B', Key K, na'|} \<in> analz (spies evs);
@@ -384,6 +397,7 @@
lemma Auth_A_to_B_lemma [rule_format]:
"evs \<in> yahalom
==> Key K \<notin> analz (knows Spy evs) -->
+ K \<in> symKeys -->
Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}
\<in> parts (knows Spy evs) -->
@@ -392,13 +406,14 @@
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
-(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
+txt{*YM3: by @{text new_keys_not_used}, the message
+ @{term "Crypt K (Nonce NB)"} could not exist*}
apply (force dest!: Crypt_imp_keysFor)
-(*YM4: was Crypt K (Nonce NB) the very last message? If so, apply unicity
- of session keys; if not, use ind. hyp.*)
-apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys )
+txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If so,
+ apply unicity of session keys; if not, use the induction hypothesis*}
+apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
done
@@ -409,7 +424,7 @@
"[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|},
Crypt K (Nonce NB)|} \<in> set evs;
(\<forall>NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \<notin> set evs);
- A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
by (blast intro: Auth_A_to_B_lemma
dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK)
--- a/src/HOL/Auth/Yahalom_Bad.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy Fri Sep 26 10:34:28 2003 +0200
@@ -2,17 +2,17 @@
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-
-Inductive relation "yahalom" for the Yahalom protocol.
-
-Demonstrates of why Oops is necessary. This protocol can be attacked because
-it doesn't keep NB secret, but without Oops it can be "verified" anyway.
-The issues are discussed in lcp's LICS 2000 invited lecture.
*)
header{*The Yahalom Protocol: A Flawed Version*}
-theory Yahalom_Bad = Shared:
+theory Yahalom_Bad = Public:
+
+text{*
+Demonstrates of why Oops is necessary. This protocol can be attacked because
+it doesn't keep NB secret, but without Oops it can be "verified" anyway.
+The issues are discussed in lcp's LICS 2000 invited lecture.
+*}
consts yahalom :: "event list set"
inductive "yahalom"
@@ -44,7 +44,7 @@
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a packet for forwarding to Bob.*)
- YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
+ YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys;
Gets Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
\<in> set evs3 |]
@@ -56,7 +56,7 @@
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce. The premise
A \<noteq> Server is needed to prove Says_Server_not_range.*)
- YM4: "[| evs4 \<in> yahalom; A \<noteq> Server;
+ YM4: "[| evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys;
Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|}
\<in> set evs4;
Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
@@ -69,8 +69,8 @@
declare analz_into_parts [dest]
-(*A "possibility property": there are traces that reach the end*)
-lemma "[| A \<noteq> Server; Key K \<notin> used [] |]
+text{*A "possibility property": there are traces that reach the end*}
+lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
==> \<exists>X NB. \<exists>evs \<in> yahalom.
Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
apply (intro exI bexI)
@@ -82,6 +82,8 @@
apply (possibility, simp add: used_Cons)
done
+subsection{*Regularity Lemmas for Yahalom*}
+
lemma Gets_imp_Says:
"[| Gets B X \<in> set evs; evs \<in> yahalom |] ==> \<exists>A. Says A B X \<in> set evs"
by (erule rev_mp, erule yahalom.induct, auto)
@@ -94,11 +96,9 @@
declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
-(**** Inductive proofs about yahalom ****)
+subsection{* For reasoning about the encrypted portion of messages *}
-(** For reasoning about the encrypted portion of messages **)
-
-(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+text{*Lets us treat YM4 using a similar argument as for the Fake case.*}
lemma YM4_analz_knows_Spy:
"[| Gets A {|Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
==> X \<in> analz (knows Spy evs)"
@@ -108,10 +108,10 @@
YM4_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 (knows Spy 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> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
apply (erule yahalom.induct, force,
@@ -126,18 +126,21 @@
"[|Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom|] ==> A \<in> bad"
by (blast dest: Spy_see_shrK)
-(*Nobody can have used non-existent keys! Needed to apply analz_insert_Key*)
-lemma new_keys_not_used [rule_format, simp]:
- "evs \<in> yahalom ==> Key K \<notin> used evs --> K \<notin> keysFor (parts (knows Spy evs))"
+text{*Nobody can have used non-existent keys!
+ Needed to apply @{text analz_insert_Key}*}
+lemma new_keys_not_used [simp]:
+ "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom|]
+ ==> K \<notin> keysFor (parts (spies evs))"
+apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
txt{*Fake*}
-apply (force dest!: keysFor_parts_insert)
-txt{*YM3, YM4*}
-apply blast+
+apply (force dest!: keysFor_parts_insert, auto)
done
+subsection{*Secrecy Theorems*}
+
(****
The following is to prove theorems of the form
@@ -147,25 +150,24 @@
A more general formula must be proved inductively.
****)
-(** Session keys are not used to encrypt other session keys **)
+subsection{* Session keys are not used to encrypt other session keys *}
lemma analz_image_freshK [rule_format]:
"evs \<in> yahalom ==>
\<forall>K KK. KK <= - (range shrK) -->
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
-apply (erule yahalom.induct, force,
- drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
-done
+by (erule yahalom.induct,
+ drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast)
-lemma analz_insert_freshK: "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
+lemma analz_insert_freshK:
+ "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
(K = KAB | Key K \<in> analz (knows Spy evs))"
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 A
{|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \<in> set evs;
@@ -175,13 +177,12 @@
==> A=A' & B=B' & na=na' & nb=nb'"
apply (erule rev_mp, erule rev_mp)
apply (erule yahalom.induct, simp_all)
-(*YM3, by freshness, and YM4*)
+txt{*YM3, by freshness, and YM4*}
apply blast+
done
-(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
-
+text{* Crucial secrecy property: Spy does not see the keys sent in msg YM3 *}
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Says Server A
@@ -194,7 +195,7 @@
apply (blast dest: unique_session_keys) (*YM3*)
done
-(*Final version*)
+text{*Final version*}
lemma Spy_not_see_encrypted_key:
"[| Says Server A
{|Crypt (shrK A) {|Agent B, Key K, na, nb|},
@@ -205,9 +206,9 @@
by (blast dest: secrecy_lemma)
-(** Security Guarantee for A upon receiving YM3 **)
+subsection{* Security Guarantee for A upon receiving YM3 *}
-(*If the encrypted message appears then it originated with the Server*)
+text{*If the encrypted message appears then it originated with the Server*}
lemma A_trusts_YM3:
"[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
A \<notin> bad; evs \<in> yahalom |]
@@ -218,21 +219,22 @@
apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3*)
+txt{*Fake, YM3*}
apply blast+
done
-(*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text A_trusts_YM3} with
+ @{text Spy_not_see_encrypted_key}*}
lemma A_gets_good_key:
"[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \<in> parts (knows Spy evs);
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
-(** Security Guarantees for B upon receiving YM4 **)
+subsection{* Security Guarantees for B upon receiving YM4 *}
-(*B knows, by the first part of A's message, that the Server distributed
- the key for A and B. But this part says nothing about nonces.*)
+text{*B knows, by the first part of A's message, that the Server distributed
+ the key for A and B. But this part says nothing about nonces.*}
lemma B_trusts_YM4_shrK:
"[| Crypt (shrK B) {|Agent A, Key K|} \<in> parts (knows Spy evs);
B \<notin> bad; evs \<in> yahalom |]
@@ -243,19 +245,21 @@
apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-(*Fake, YM3*)
+txt{*Fake, YM3*}
apply blast+
done
-(** Up to now, the reasoning is similar to standard Yahalom. Now the
+subsection{*The Flaw in the Model*}
+
+text{* Up to now, the reasoning is similar to standard Yahalom. Now the
doubtful reasoning occurs. We should not be assuming that an unknown
key is secure, but the model allows us to: there is no Oops rule to
- let session keys become compromised.*)
+ let session keys become compromised.*}
-(*B knows, by the second part of A's message, that the Server distributed
+text{*B knows, by the second part of A's message, that the Server distributed
the key quoting nonce NB. This part says nothing about agent names.
Secrecy of K is assumed; the valid Yahalom proof uses (and later proves)
- the secrecy of NB.*)
+ the secrecy of NB.*}
lemma B_trusts_YM4_newK [rule_format]:
"[|Key K \<notin> analz (knows Spy evs); evs \<in> yahalom|]
==> Crypt K (Nonce NB) \<in> parts (knows Spy evs) -->
@@ -268,20 +272,20 @@
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
-(*YM3*)
+txt{*YM3*}
apply blast
-(*A is uncompromised because NB is secure
- A's certificate guarantees the existence of the Server message*)
+txt{*A is uncompromised because NB is secure
+ A's certificate guarantees the existence of the Server message*}
apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
dest: Says_imp_spies
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3])
done
-(*B's session key guarantee from YM4. The two certificates contribute to a
- single conclusion about the Server's message. *)
+text{*B's session key guarantee from YM4. The two certificates contribute to a
+ single conclusion about the Server's message. *}
lemma B_trusts_YM4:
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
Crypt K (Nonce NB)|} \<in> set evs;
@@ -297,7 +301,8 @@
unique_session_keys)
-(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
+text{*The obvious combination of @{text B_trusts_YM4} with
+ @{text Spy_not_see_encrypted_key}*}
lemma B_gets_good_key:
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
Crypt K (Nonce NB)|} \<in> set evs;
@@ -315,9 +320,9 @@
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
-(*Assuming the session key is secure, if both certificates are present then
+text{*Assuming the session key is secure, if both certificates are present then
A has said NB. We can't be sure about the rest of A's message, but only
- NB matters for freshness.*)
+ NB matters for freshness.*}
lemma A_Said_YM3_lemma [rule_format]:
"evs \<in> yahalom
==> Key K \<notin> analz (knows Spy evs) -->
@@ -328,21 +333,23 @@
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
-(*Fake*)
+txt{*Fake*}
apply blast
-(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
+txt{*YM3: by @{text new_keys_not_used}, the message
+ @{term "Crypt K (Nonce NB)"} could not exist*}
apply (force dest!: Crypt_imp_keysFor)
-(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*)
+txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message?
+ If not, use the induction hypothesis*}
apply (simp add: ex_disj_distrib)
-(*yes: apply unicity of session keys*)
+txt{*yes: apply unicity of session keys*}
apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK
Crypt_Spy_analz_bad
dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
done
-(*If B receives YM4 then A has used nonce NB (and therefore is alive).
+text{*If B receives YM4 then A has used nonce NB (and therefore is alive).
Moreover, A associates K with NB (thus is talking about the same run).
- Other premises guarantee secrecy of K.*)
+ Other premises guarantee secrecy of K.*}
lemma YM4_imp_A_Said_YM3 [rule_format]:
"[| Gets B {|Crypt (shrK B) {|Agent A, Key K|},
Crypt K (Nonce NB)|} \<in> set evs;
@@ -351,8 +358,7 @@
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
==> \<exists>X. Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
-apply (blast intro!: A_Said_YM3_lemma
- dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
-done
+by (blast intro!: A_Said_YM3_lemma
+ dest: Spy_not_see_encrypted_key B_trusts_YM4 Gets_imp_Says)
end
--- a/src/HOL/Auth/ZhouGollmann.thy Fri Sep 26 10:32:26 2003 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy Fri Sep 26 10:34:28 2003 +0200
@@ -16,7 +16,7 @@
TTP :: agent
translations
- "TTP" == "Server"
+ "TTP" == "Server "
syntax
f_sub :: nat