--- a/src/HOL/Auth/OtwayRees.thy Wed Apr 09 12:51:49 2003 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Wed Apr 09 12:52:45 2003 +0200
@@ -3,18 +3,17 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-Inductive relation "otway" for the Otway-Rees protocol
-extended by Gets primitive.
-
-Version that encrypts Nonce NB
From page 244 of
Burrows, Abadi and Needham. A Logic of Authentication.
Proc. Royal Soc. 426 (1989)
*)
+header{*Verifying the Otway-Rees protocol*}
+
theory OtwayRees = Shared:
+text{*This is the original version, which encrypts Nonce NB.*}
consts otway :: "event list set"
inductive "otway"
@@ -89,7 +88,7 @@
declare Fake_parts_insert_in_Un [dest]
-(*A "possibility property": there are traces that reach the end*)
+text{*A "possibility property": there are traces that reach the end*}
lemma "B \<noteq> Server
==> \<exists>K. \<exists>evs \<in> otway.
Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|}
@@ -98,7 +97,8 @@
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4],
+ possibility)
done
lemma Gets_imp_Says [dest!]:
@@ -138,9 +138,9 @@
(*Spy never sees a good agent's shared key!*)
lemma Spy_see_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
-apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
-done
+by (erule otway.induct, force,
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
+
lemma Spy_analz_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)"
@@ -151,7 +151,7 @@
by (blast dest: Spy_see_shrK)
-(*** Proofs involving analz ***)
+subsection{*Towards Secrecy: Proofs Involving @{term analz}*}
(*Describes the form of K and NA when the Server sends this message. Also
for Oops case.*)
@@ -159,8 +159,7 @@
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
-apply (erule rev_mp, erule otway.induct, simp_all, blast)
-done
+by (erule rev_mp, erule otway.induct, simp_all, blast)
(****
@@ -173,7 +172,7 @@
****)
-(** Session keys are not used to encrypt other session keys **)
+text{*Session keys are not used to encrypt other session keys*}
(*The equality makes the induction hypothesis easier to apply*)
lemma analz_image_freshK [rule_format]:
@@ -209,7 +208,7 @@
done
-(**** Authenticity properties relating to NA ****)
+subsection{*Authenticity properties relating to NA*}
(*Only OR1 can have caused such a part of a message to appear.*)
lemma Crypt_imp_OR1 [rule_format]:
@@ -232,8 +231,7 @@
by (blast dest: Crypt_imp_OR1)
-(** The Nonce NA uniquely identifies A's message. **)
-
+text{*The Nonce NA uniquely identifies A's message*}
lemma unique_NA:
"[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs);
Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs);
@@ -316,7 +314,7 @@
apply (blast dest: unique_session_keys)+
done
-lemma Spy_not_see_encrypted_key:
+theorem Spy_not_see_encrypted_key:
"[| Says Server B
{|NA, Crypt (shrK A) {|NA, Key K|},
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
@@ -325,6 +323,22 @@
==> Key K \<notin> analz (knows Spy evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)
+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 "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
+other than Fake are trivial, while Fake requires
+@{term "Key K \<notin> analz (knows Spy evs)"}. *}
+lemma Spy_not_know_encrypted_key:
+ "[| Says Server B
+ {|NA, Crypt (shrK A) {|NA, Key K|},
+ Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
+ Notes Spy {|NA, NB, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> otway |]
+ ==> Key K \<notin> knows Spy evs"
+by (blast dest: Spy_not_see_encrypted_key)
+
(*A's guarantee. The Oops premise quantifies over NB because A cannot know
what it is.*)
@@ -339,7 +353,7 @@
-(**** Authenticity properties relating to NB ****)
+subsection{*Authenticity properties relating to NB*}
(*Only OR2 can have caused such a part of a message to appear. We do not
know anything about X: it does NOT have to have the right form.*)
@@ -356,8 +370,7 @@
done
-(** The Nonce NB uniquely identifies B's message. **)
-
+text{*The Nonce NB uniquely identifies B's message*}
lemma unique_NB:
"[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \<in> parts(knows Spy evs);
Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \<in> parts(knows Spy evs);
@@ -396,9 +409,9 @@
done
-(*Guarantee for B: if it gets a message with matching NB then the Server
- has sent the correct message.*)
-lemma B_trusts_OR3:
+text{*Guarantee for B: if it gets a message with matching NB then the Server
+ has sent the correct message.*}
+theorem B_trusts_OR3:
"[| Says B Server {|NA, Agent A, Agent B, X',
Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}
\<in> set evs;
@@ -438,10 +451,10 @@
done
-(*After getting and checking OR4, agent A can trust that B has been active.
+text{*After getting and checking OR4, agent A can trust that B has been active.
We could probably prove that X has the expected form, but that is not
- strictly necessary for authentication.*)
-lemma A_auths_B:
+ strictly necessary for authentication.*}
+theorem A_auths_B:
"[| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} \<in> set evs;
Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs;
--- a/src/HOL/Auth/Shared.thy Wed Apr 09 12:51:49 2003 +0200
+++ b/src/HOL/Auth/Shared.thy Wed Apr 09 12:52:45 2003 +0200
@@ -46,7 +46,7 @@
method_setup analz_freshK = {*
Method.no_args
(Method.METHOD
- (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, impI]),
+ (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"
--- a/src/HOL/Auth/Yahalom2.thy Wed Apr 09 12:51:49 2003 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Wed Apr 09 12:52:45 2003 +0200
@@ -3,8 +3,6 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
-Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
-
This version trades encryption of NB for additional explicitness in YM3.
Also in YM3, care is taken to make the two certificates distinct.
@@ -13,6 +11,8 @@
Proc. Royal Soc. 426 (1989)
*)
+header{*Inductive Analysis of the Yahalom protocol, Variant 2*}
+
theory Yahalom2 = Shared:
consts yahalom :: "event list set"
@@ -79,7 +79,7 @@
declare Fake_parts_insert_in_Un [dest]
declare analz_into_parts [dest]
-(*A "possibility property": there are traces that reach the end*)
+text{*A "possibility property": there are traces that reach the end*}
lemma "\<exists>X NB K. \<exists>evs \<in> yahalom.
Says A B {|X, Crypt K (Nonce NB)|} \<in> set evs"
apply (intro exI bexI)
@@ -94,7 +94,7 @@
"[| 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)
@@ -102,11 +102,10 @@
declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
-(**** Inductive proofs about yahalom ****)
+subsection{*Inductive Proofs*}
-(** For reasoning about the encrypted portion of messages **)
-
-(*Lets us treat YM4 using a similar argument as for the Fake case.*)
+text{*Result for reasoning about the encrypted portion of messages.
+Lets us treat YM4 using a similar argument as for the Fake case.*}
lemma YM4_analz_knows_Spy:
"[| Gets A {|NB, Crypt (shrK A) Y, X|} \<in> set evs; evs \<in> yahalom |]
==> X \<in> analz (knows Spy evs)"
@@ -119,12 +118,11 @@
(** Theorems of the form 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)"
@@ -180,8 +178,7 @@
by (simp only: analz_image_freshK analz_image_freshK_simps)
-(*** The Key K uniquely identifies the Server's message. **)
-
+text{*The Key K uniquely identifies the Server's message*}
lemma unique_session_keys:
"[| Says Server A
{|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} \<in> set evs;
@@ -191,12 +188,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*)
+txt{*YM3, by freshness*}
apply blast
done
-(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
+subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*}
lemma secrecy_lemma:
"[| A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
@@ -208,7 +205,7 @@
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz)
apply (blast dest: unique_session_keys)+ (*YM3, Oops*)
done
@@ -225,7 +222,26 @@
by (blast dest: secrecy_lemma Says_Server_message_form)
-(** Security Guarantee for A upon receiving YM3 **)
+
+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 "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases
+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
+ {|nb, Crypt (shrK A) {|Agent B, Key K, na|},
+ Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}
+ \<in> set evs;
+ Notes Spy {|na, nb, Key K|} \<notin> set evs;
+ A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
+ ==> Key K \<notin> knows Spy evs"
+by (blast dest: Spy_not_see_encrypted_key)
+
+
+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.*)
@@ -239,12 +255,12 @@
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*)
-lemma A_gets_good_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;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
@@ -252,7 +268,7 @@
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key)
-(** Security Guarantee for B upon receiving YM4 **)
+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.*)
@@ -291,7 +307,7 @@
(*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
-lemma B_gets_good_key:
+theorem B_gets_good_key:
"[| Gets B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, X|}
\<in> set evs;
\<forall>na. Notes Spy {|na, Nonce NB, Key K|} \<notin> set evs;
@@ -300,7 +316,7 @@
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.*)
lemma B_Said_YM2:
@@ -331,8 +347,8 @@
apply (blast dest!: B_Said_YM2)+
done
-(*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
-lemma YM3_auth_B_to_A:
+text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*}
+theorem YM3_auth_B_to_A:
"[| Gets A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|}
\<in> set evs;
A \<notin> bad; B \<notin> bad; evs \<in> yahalom |]
@@ -342,8 +358,9 @@
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma)
+subsection{*Authenticating A to B*}
-(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
+text{*using the certificate @{term "Crypt K (Nonce NB)"}*}
(*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
@@ -381,10 +398,10 @@
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.*)
-lemma YM4_imp_A_Said_YM3 [rule_format]:
+ Other premises guarantee secrecy of K.*}
+theorem YM4_imp_A_Said_YM3 [rule_format]:
"[| 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);