diff -r 55c85d25e18c -r 4f5ab843cf5b src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Thu Dec 10 21:31:24 2015 +0100 +++ b/src/HOL/Auth/Yahalom.thy Thu Dec 10 21:39:33 2015 +0100 @@ -3,16 +3,16 @@ Copyright 1996 University of Cambridge *) -section{*The Yahalom Protocol*} +section\The Yahalom Protocol\ theory Yahalom imports Public begin -text{*From page 257 of +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. -*} +\ inductive_set yahalom :: "event list set" where @@ -53,10 +53,10 @@ # evs3 \ yahalom" | YM4: - --{*Alice receives the Server's (?) message, checks her Nonce, and + \\Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce. The premise - @{term "A \ Server"} is needed for @{text Says_Server_not_range}. - Alice can check that K is symmetric by its length.*} + @{term "A \ Server"} is needed for \Says_Server_not_range\. + Alice can check that K is symmetric by its length.\ "[| evs4 \ yahalom; A \ Server; K \ symKeys; Gets A {|Crypt(shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} \ set evs4; @@ -85,7 +85,7 @@ declare Fake_parts_insert_in_Un [dest] declare analz_into_parts [dest] -text{*A "possibility property": there are traces that reach the end*} +text\A "possibility property": there are traces that reach the end\ lemma "[| A \ Server; K \ symKeys; Key K \ used [] |] ==> \X NB. \evs \ yahalom. Says A B {|X, Crypt K (Nonce NB)|} \ set evs" @@ -99,13 +99,13 @@ done -subsection{*Regularity Lemmas for Yahalom*} +subsection\Regularity Lemmas for Yahalom\ lemma Gets_imp_Says: "[| Gets B X \ set evs; evs \ yahalom |] ==> \A. Says A B X \ set evs" by (erule rev_mp, erule yahalom.induct, auto) -text{*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) @@ -114,7 +114,7 @@ declare Gets_imp_analz_Spy [dest] -text{*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|} \ set evs; evs \ yahalom |] ==> X \ analz (knows Spy evs)" @@ -123,16 +123,16 @@ lemmas YM4_parts_knows_Spy = YM4_analz_knows_Spy [THEN analz_into_parts] -text{*For Oops*} +text\For Oops\ lemma YM4_Key_parts_knows_Spy: "Says Server A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} \ set evs ==> K \ parts (knows Spy evs)" by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) -text{*Theorems of the form @{term "X \ parts (knows Spy evs)"} imply -that NOBODY sends messages containing X! *} +text\Theorems of the form @{term "X \ parts (knows Spy evs)"} imply +that NOBODY sends messages containing X!\ -text{*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)" by (erule yahalom.induct, force, @@ -146,29 +146,29 @@ "[|Key (shrK A) \ parts (knows Spy evs); evs \ yahalom|] ==> A \ bad" by (blast dest: Spy_see_shrK) -text{*Nobody can have used non-existent keys! - Needed to apply @{text analz_insert_Key}*} +text\Nobody can have used non-existent keys! + Needed to apply \analz_insert_Key\\ lemma new_keys_not_used [simp]: "[|Key K \ used evs; K \ symKeys; evs \ yahalom|] ==> K \ keysFor (parts (spies evs))" apply (erule rev_mp) apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy, simp_all) -txt{*Fake*} +txt\Fake\ apply (force dest!: keysFor_parts_insert, auto) done -text{*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: "[|K \ symKeys; evs \ yahalom; Key K \ used evs|] ==> K \ keysFor (analz (knows Spy evs))" by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) -text{*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|} \ set evs; evs \ yahalom |] @@ -176,7 +176,7 @@ by (erule rev_mp, erule yahalom.induct, simp_all) -subsection{*Secrecy Theorems*} +subsection\Secrecy Theorems\ (**** The following is to prove theorems of the form @@ -187,7 +187,7 @@ A more general formula must be proved inductively. ****) -text{* 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 \ yahalom ==> @@ -207,7 +207,7 @@ by (simp only: analz_image_freshK analz_image_freshK_simps) -text{*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|} \ set evs; @@ -217,12 +217,12 @@ ==> A=A' & B=B' & na=na' & nb=nb'" apply (erule rev_mp, erule rev_mp) apply (erule yahalom.induct, simp_all) -txt{*YM3, by freshness, and YM4*} +txt\YM3, by freshness, and YM4\ apply blast+ done -text{*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 \ bad; B \ bad; evs \ yahalom |] ==> Says Server A @@ -233,11 +233,11 @@ Key K \ analz (knows Spy evs)" 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 -text{*Final version*} +text\Final version\ lemma Spy_not_see_encrypted_key: "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, @@ -249,9 +249,9 @@ by (blast dest: secrecy_lemma) -subsubsection{* Security Guarantee for A upon receiving YM3 *} +subsubsection\Security Guarantee for A upon receiving YM3\ -text{*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|} \ parts (knows Spy evs); A \ bad; evs \ yahalom |] @@ -262,12 +262,12 @@ apply (erule rev_mp) apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy, simp_all) -txt{*Fake, YM3*} +txt\Fake, YM3\ apply blast+ done -text{*The obvious combination of @{text A_trusts_YM3} with - @{text Spy_not_see_encrypted_key}*} +text\The obvious combination of \A_trusts_YM3\ with + \Spy_not_see_encrypted_key\\ lemma A_gets_good_key: "[| Crypt (shrK A) {|Agent B, Key K, na, nb|} \ parts (knows Spy evs); Notes Spy {|na, nb, Key K|} \ set evs; @@ -276,10 +276,10 @@ by (metis A_trusts_YM3 secrecy_lemma) -subsubsection{* Security Guarantees for B upon receiving YM4 *} +subsubsection\Security Guarantees for B upon receiving YM4\ -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.*} +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|} \ parts (knows Spy evs); B \ bad; evs \ yahalom |] @@ -291,15 +291,15 @@ apply (erule rev_mp) apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy, simp_all) -txt{*Fake, YM3*} +txt\Fake, YM3\ apply blast+ done -text{*B knows, by the second part of A's message, that the Server +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 @{term "Nonce NB \ analz(knows Spy evs)"} must be the FIRST antecedent of the - induction formula.*} + induction formula.\ lemma B_trusts_YM4_newK [rule_format]: "[|Crypt K (Nonce NB) \ parts (knows Spy evs); @@ -312,20 +312,20 @@ apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy) apply (analz_mono_contra, simp_all) -txt{*Fake, YM3*} +txt\Fake, YM3\ apply blast apply blast -txt{*YM4. A is uncompromised because NB is secure - A's certificate guarantees the existence of the Server message*} +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 -subsubsection{* Towards proving secrecy of Nonce NB *} +subsubsection\Towards proving secrecy of Nonce NB\ -text{*Lemmas about the predicate KeyWithNonce*} +text\Lemmas about the predicate KeyWithNonce\ lemma KeyWithNonceI: "Says Server A @@ -349,14 +349,14 @@ "KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" by (simp add: KeyWithNonce_def) -text{*A fresh key cannot be associated with any nonce - (with respect to a given trace). *} +text\A fresh key cannot be associated with any nonce + (with respect to a given trace).\ lemma fresh_not_KeyWithNonce: "Key K \ used evs ==> ~ KeyWithNonce K NB evs" by (unfold KeyWithNonce_def, blast) -text{*The Server message associates K with NB' and therefore not with any - other nonce NB.*} +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|} \ set evs; @@ -365,13 +365,13 @@ by (unfold KeyWithNonce_def, blast dest: unique_session_keys) -text{*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 @{text analz_image_freshK}, but it is much more complicated.*} + recalls \analz_image_freshK\, but it is much more complicated.\ -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.*} +text\As with \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 \ analz (G Un H)) --> (X \ analz H) ==> P --> (X \ analz (G Un H)) = (X \ analz H)" @@ -392,29 +392,29 @@ analz_image_freshK fresh_not_KeyWithNonce imp_disj_not1 (*Moves NBa\NB to the front*) Says_Server_KeyWithNonce) -txt{*For Oops, simplification proves @{prop "NBa\NB"}. By +txt\For Oops, simplification proves @{prop "NBa\NB"}. By @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB evs"}; then simplification can apply the induction hypothesis with - @{term "KK = {K}"}.*} -txt{*Fake*} + @{term "KK = {K}"}.\ +txt\Fake\ apply spy_analz -txt{*YM2*} +txt\YM2\ apply blast -txt{*YM3*} +txt\YM3\ apply blast -txt{*YM4*} +txt\YM4\ apply (erule_tac V = "\KK. P KK" for P in thin_rl, clarify) -txt{*If @{prop "A \ bad"} then @{term NBa} is known, therefore +txt\If @{prop "A \ bad"} then @{term NBa} is known, therefore @{prop "NBa \ NB"}. Previous two steps make the next step - faster.*} + faster.\ apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) done -text{*Version required below: if NB can be decrypted using a session key then +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.*} + for the induction to carry through.\ lemma single_Nonce_secrecy: "[| Says Server A {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|} @@ -427,7 +427,7 @@ Nonce_secrecy Says_Server_KeyWithNonce) -subsubsection{* 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|} \ parts (knows Spy evs); @@ -437,13 +437,13 @@ apply (erule rev_mp, erule rev_mp) apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy, simp_all) -txt{*Fake, and YM2 by freshness*} +txt\Fake, and YM2 by freshness\ apply blast+ done -text{*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|}|} \ set evs; @@ -455,7 +455,7 @@ dest: Says_imp_spies unique_NB parts.Inj analz.Inj) -subsubsection{* 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'|} \ parts(knows Spy evs); @@ -465,11 +465,11 @@ apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy) apply (analz_mono_contra, simp_all) -txt{*Fake, YM2*} +txt\Fake, YM2\ apply blast+ done -text{*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|} \ set evs; evs \ yahalom |] @@ -477,7 +477,7 @@ \ set evs" by (erule rev_mp, erule yahalom.induct, auto) -text{*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|}|} @@ -490,36 +490,36 @@ frule_tac [6] YM4_analz_knows_Spy) apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq analz_insert_freshK) -txt{*Fake*} +txt\Fake\ apply spy_analz -txt{*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 -txt{*YM2*} +txt\YM2\ apply blast -txt{*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) -txt{*LEVEL 7: YM4 and Oops remain*} +txt\LEVEL 7: YM4 and Oops remain\ apply (clarify, simp add: all_conj_distrib) -txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*} -txt{*Case analysis on Aa:bad; PROOF FAILED problems - use @{text Says_unique_NB} to identify message components: @{term "Aa=A"}, @{term "Ba=B"}*} +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: @{term "Aa=A"}, @{term "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) -txt{*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 (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) done -text{*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 @{text \} POSSIBLE keys instead of our particular K. + assumption must quantify over \\\ 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)|} \ set evs; @@ -538,8 +538,8 @@ -text{*The obvious combination of @{text B_trusts_YM4} with - @{text Spy_not_see_encrypted_key}*} +text\The obvious combination of \B_trusts_YM4\ with + \Spy_not_see_encrypted_key\\ lemma B_gets_good_key: "[| Gets B {|Crypt (shrK B) {|Agent A, Key K|}, Crypt K (Nonce NB)|} \ set evs; @@ -552,9 +552,9 @@ by (metis B_trusts_YM4 Spy_not_see_encrypted_key) -subsection{*Authenticating B to A*} +subsection\Authenticating B to A\ -text{*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|} \ parts (knows Spy evs); evs \ yahalom|] @@ -563,11 +563,11 @@ \ set evs" apply (erule rev_mp, erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy, simp_all) -txt{*Fake*} +txt\Fake\ apply blast done -text{*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|} \ set evs; evs \ yahalom|] @@ -575,11 +575,11 @@ Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \ set evs" apply (erule rev_mp, erule yahalom.induct, simp_all) -txt{*YM3, YM4*} +txt\YM3, YM4\ apply (blast dest!: B_Said_YM2)+ done -text{*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|} \ set evs; @@ -590,12 +590,12 @@ not_parts_not_analz) -subsection{*Authenticating A to B using the certificate - @{term "Crypt K (Nonce NB)"}*} +subsection\Authenticating A to B using the certificate + @{term "Crypt K (Nonce NB)"}\ -text{*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 \ yahalom ==> Key K \ analz (knows Spy evs) --> @@ -606,23 +606,23 @@ apply (erule yahalom.induct, force, frule_tac [6] YM4_parts_knows_Spy) apply (analz_mono_contra, simp_all) -txt{*Fake*} +txt\Fake\ apply blast -txt{*YM3: by @{text new_keys_not_used}, the message - @{term "Crypt K (Nonce NB)"} could not exist*} +txt\YM3: by \new_keys_not_used\, the message + @{term "Crypt K (Nonce NB)"} could not exist\ apply (force dest!: Crypt_imp_keysFor) -txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message? - If not, use the induction hypothesis*} +txt\YM4: was @{term "Crypt K (Nonce NB)"} the very last message? + If not, use the induction hypothesis\ apply (simp add: ex_disj_distrib) -txt{*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 -text{*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)|} \ set evs;