# HG changeset patch # User paulson # Date 1049885565 -7200 # Node ID 2bc462b99e709ad440a08a29f0d476aa4b82e255 # Parent eefdd6b14508407cbba9267522b2f6f73f375900 tidying diff -r eefdd6b14508 -r 2bc462b99e70 src/HOL/Auth/OtwayRees.thy --- 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 \ Server ==> \K. \evs \ 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 \ otway ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ 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 \ otway ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ 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|}|} \ set evs; evs \ otway |] ==> K \ range shrK & (\i. NA = Nonce i) & (\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|} \ parts (knows Spy evs); Crypt (shrK A) {|NA, Agent A, Agent C|} \ 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|}|} \ set evs; @@ -325,6 +323,22 @@ ==> Key K \ 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 \ knows Spy evs"} appears not to be inductive: all the cases +other than Fake are trivial, while Fake requires +@{term "Key K \ 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|}|} \ set evs; + Notes Spy {|NA, NB, Key K|} \ set evs; + A \ bad; B \ bad; evs \ otway |] + ==> Key K \ 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|} \ parts(knows Spy evs); Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \ 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|} |} \ 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|}|} \ set evs; Says A B {|NA, Agent A, Agent B, Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ set evs; diff -r eefdd6b14508 -r 2bc462b99e70 src/HOL/Auth/Shared.thy --- 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" diff -r eefdd6b14508 -r 2bc462b99e70 src/HOL/Auth/Yahalom2.thy --- 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 "\X NB K. \evs \ yahalom. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" apply (intro exI bexI) @@ -94,7 +94,7 @@ "[| Gets B X \ set evs; evs \ yahalom |] ==> \A. Says A B X \ 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 \ set evs; evs \ yahalom |] ==> X \ 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|} \ set evs; evs \ yahalom |] ==> X \ analz (knows Spy evs)" @@ -119,12 +118,11 @@ (** Theorems of the form X \ 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 \ yahalom ==> (Key (shrK A) \ parts (knows Spy evs)) = (A \ 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 \ yahalom ==> (Key (shrK A) \ analz (knows Spy evs)) = (A \ 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|} \ 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 \ bad; B \ bad; evs \ yahalom |] @@ -208,7 +205,7 @@ Key K \ 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 \ knows Spy evs"} appears not to be inductive: all the cases +other than Fake are trivial, while Fake requires +@{term "Key K \ 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|}|} + \ set evs; + Notes Spy {|na, nb, Key K|} \ set evs; + A \ bad; B \ bad; evs \ yahalom |] + ==> Key K \ 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|} \ parts (knows Spy evs); \nb. Notes Spy {|na, nb, Key K|} \ set evs; A \ bad; B \ bad; evs \ 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|} \ set evs; \na. Notes Spy {|na, Nonce NB, Key K|} \ 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|} \ set evs; A \ bad; B \ bad; evs \ 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)|} \ set evs; (\NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} \ set evs);