# HG changeset patch # User paulson # Date 1665755868 -3600 # Node ID efc220128637a326e2cae31b4e9800a449423338 # Parent eb30869e72289fe05186d9f7067f9727d010a9fc# Parent e7f9e5b3a36a24c84a00e42d88bf06deac4d0f64 merged diff -r eb30869e7228 -r efc220128637 src/HOL/Auth/NS_Public.thy --- a/src/HOL/Auth/NS_Public.thy Fri Oct 14 14:39:52 2022 +0200 +++ b/src/HOL/Auth/NS_Public.thy Fri Oct 14 14:57:48 2022 +0100 @@ -1,189 +1,194 @@ -(* Title: HOL/Auth/NS_Public.thy +(* Title: HOL/Auth/NS_PublicX.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge - -Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. -Version incorporating Lowe's fix (inclusion of B's identity in round 2). *) -section\Verifying the Needham-Schroeder-Lowe Public-Key Protocol\ +section\Verifying the Needham-Schroeder Public-Key Protocol\ + +text \Flawed version, vulnerable to Lowe's attack. +From Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989), p. 260\ theory NS_Public imports Public begin inductive_set ns_public :: "event list set" - where - (*Initial trace is empty*) + where Nil: "[] \ ns_public" - - (*The spy MAY say anything he CAN say. We do not expect him to - invent new nonces here, but he can also use NS1. Common to - all similar protocols.*) + \ \Initial trace is empty\ | Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\ \ Says Spy B X # evsf \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) + \ \The spy can say almost anything.\ | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) - # evs1 \ ns_public" - - (*Bob responds to Alice's message with a further nonce*) + # evs1 \ ns_public" + \ \Alice initiates a protocol run, sending a nonce to Bob\ | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) + \ \Bob responds to Alice's message with a further nonce\ | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; - Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) - \ set evs3\ + Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs3\ \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" + \ \Alice proves her existence by sending @{term NB} back to Bob.\ declare knows_Spy_partsEs [elim] -declare knows_Spy_partsEs [elim] declare analz_into_parts [dest] declare Fake_parts_insert_in_Un [dest] -(*A "possibility property": there are traces that reach the end*) +text \A "possibility property": there are traces that reach the end\ lemma "\NB. \evs \ ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \ 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], possibility) -done + apply (intro exI bexI) + apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, THEN ns_public.NS3]) + by possibility + + +subsection \Inductive proofs about @{term ns_public}\ (** Theorems of the form X \ parts (spies evs) imply that NOBODY sends messages containing X! **) -(*Spy never sees another agent's private key! (unless it's bad at start)*) -lemma Spy_see_priEK [simp]: - "evs \ ns_public \ (Key (priEK A) \ parts (spies evs)) = (A \ bad)" -by (erule ns_public.induct, auto) +text \Spy never sees another agent's private key! (unless it's bad at start)\ +lemma Spy_see_priEK [simp]: + "evs \ ns_public \ (Key (priEK A) \ parts (spies evs)) = (A \ bad)" + by (erule ns_public.induct, auto) + +lemma Spy_analz_priEK [simp]: + "evs \ ns_public \ (Key (priEK A) \ analz (spies evs)) = (A \ bad)" + by auto + -lemma Spy_analz_priEK [simp]: - "evs \ ns_public \ (Key (priEK A) \ analz (spies evs)) = (A \ bad)" -by auto +subsection \Authenticity properties obtained from {term NS1}\ -subsection\Authenticity properties obtained from NS2\ +text \It is impossible to re-use a nonce in both {term NS1} and {term NS2}, provided the nonce + is secret. (Honest users generate fresh nonces.)\ +lemma no_nonce_NS1_NS2 [rule_format]: + "evs \ ns_public + \ Crypt (pubEK C) \NA', Nonce NA, Agent D\ \ parts (spies evs) \ + Crypt (pubEK B) \Nonce NA, Agent A\ \ parts (spies evs) \ + Nonce NA \ analz (spies evs)" + by (induct rule: ns_public.induct) (auto intro: analz_insertI) -(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce - is secret. (Honest users generate fresh nonces.)*) -lemma no_nonce_NS1_NS2 [rule_format]: - "evs \ ns_public - \ Crypt (pubEK C) \NA', Nonce NA, Agent D\ \ parts (spies evs) \ - Crypt (pubEK B) \Nonce NA, Agent A\ \ parts (spies evs) \ - Nonce NA \ analz (spies evs)" -apply (erule ns_public.induct, simp_all) -apply (blast intro: analz_insertI)+ -done - -(*Unicity for NS1: nonce NA identifies agents A and B*) -lemma unique_NA: - "\Crypt(pubEK B) \Nonce NA, Agent A \ \ parts(spies evs); - Crypt(pubEK B') \Nonce NA, Agent A'\ \ parts(spies evs); - Nonce NA \ analz (spies evs); evs \ ns_public\ - \ A=A' \ B=B'" -apply (erule rev_mp, erule rev_mp, erule rev_mp) -apply (erule ns_public.induct, simp_all) -(*Fake, NS1*) -apply (blast intro: analz_insertI)+ -done +text \Unicity for {term NS1}: nonce {term NA} identifies agents {term A} and {term B}\ +lemma unique_NA: + assumes NA: "Crypt(pubEK B) \Nonce NA, Agent A \ \ parts(spies evs)" + "Crypt(pubEK B') \Nonce NA, Agent A'\ \ parts(spies evs)" + "Nonce NA \ analz (spies evs)" + and evs: "evs \ ns_public" + shows "A=A' \ B=B'" + using evs NA + by (induction rule: ns_public.induct) (auto intro!: analz_insertI split: if_split_asm) -(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure - The major premise "Says A B ..." makes it a dest-rule, so we use - (erule rev_mp) rather than rule_format. *) -theorem Spy_not_see_NA: - "\Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ - \ Nonce NA \ analz (spies evs)" -apply (erule rev_mp) -apply (erule ns_public.induct, simp_all, spy_analz) -apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ -done +text \Secrecy: Spy does not see the nonce sent in msg {term NS1} if {term A} and {term B} are secure + The major premise "Says A B ..." makes it a dest-rule, hence the given assumption order. \ +theorem Spy_not_see_NA: + assumes NA: "Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs" + "A \ bad" "B \ bad" + and evs: "evs \ ns_public" + shows "Nonce NA \ analz (spies evs)" + using evs NA +proof (induction rule: ns_public.induct) + case (Fake evsf X B) + then show ?case + by spy_analz +next + case (NS2 evs2 NB A' B NA A) + then show ?case + by simp (metis Says_imp_analz_Spy analz_into_parts parts.simps unique_NA usedI) +next + case (NS3 evs3 A B NA B' NB) + then show ?case + by simp (meson Says_imp_analz_Spy analz_into_parts no_nonce_NS1_NS2) +qed auto -(*Authentication for A: if she receives message 2 and has used NA - to start a run, then B has sent message 2.*) -lemma A_trusts_NS2_lemma [rule_format]: - "\A \ bad; B \ bad; evs \ ns_public\ +text \Authentication for {term A}: if she receives message 2 and has used {term NA} + to start a run, then {term B} has sent message 2.\ +lemma A_trusts_NS2_lemma [rule_format]: + "\A \ bad; B \ bad; evs \ ns_public\ \ Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\ \ parts (spies evs) \ Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs \ Says B A (Crypt(pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs" -apply (erule ns_public.induct, simp_all) -(*Fake, NS1*) -apply (blast dest: Spy_not_see_NA)+ -done + by (erule ns_public.induct) (auto dest: Spy_not_see_NA unique_NA) -theorem A_trusts_NS2: - "\Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs; +theorem A_trusts_NS2: + "\Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs; Says B' A (Crypt(pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ + A \ bad; B \ bad; evs \ ns_public\ \ Says B A (Crypt(pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs" -by (blast intro: A_trusts_NS2_lemma) + by (blast intro: A_trusts_NS2_lemma) -(*If the encrypted message appears then it originated with Alice in NS1*) +text \If the encrypted message appears then it originated with Alice in {term NS1}\ lemma B_trusts_NS1 [rule_format]: - "evs \ ns_public + "evs \ ns_public \ Crypt (pubEK B) \Nonce NA, Agent A\ \ parts (spies evs) \ Nonce NA \ analz (spies evs) \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs" -apply (erule ns_public.induct, simp_all) -(*Fake*) -apply (blast intro!: analz_insertI) -done + by (induction evs rule: ns_public.induct) (use analz_insertI in auto) + + +subsection \Authenticity properties obtained from {term NS2}\ + +text \Unicity for {term NS2}: nonce {term NB} identifies nonce {term NA} and agent {term A} + [proof closely follows that for @{thm [source] unique_NA}]\ + +lemma unique_NB [dest]: + assumes NB: "Crypt(pubEK A) \Nonce NA, Nonce NB, Agent B\ \ parts(spies evs)" + "Crypt(pubEK A') \Nonce NA', Nonce NB, Agent B'\ \ parts(spies evs)" + "Nonce NB \ analz (spies evs)" + and evs: "evs \ ns_public" + shows "A=A' \ NA=NA' \ B=B'" + using evs NB + by (induction rule: ns_public.induct) (auto intro!: analz_insertI split: if_split_asm) -subsection\Authenticity properties obtained from NS2\ - -(*Unicity for NS2: nonce NB identifies nonce NA and agents A, B - [unicity of B makes Lowe's fix work] - [proof closely follows that for unique_NA] *) - -lemma unique_NB [dest]: - "\Crypt(pubEK A) \Nonce NA, Nonce NB, Agent B\ \ parts(spies evs); - Crypt(pubEK A') \Nonce NA', Nonce NB, Agent B'\ \ parts(spies evs); - Nonce NB \ analz (spies evs); evs \ ns_public\ - \ A=A' \ NA=NA' \ B=B'" -apply (erule rev_mp, erule rev_mp, erule rev_mp) -apply (erule ns_public.induct, simp_all) -(*Fake, NS2*) -apply (blast intro: analz_insertI)+ -done +text \{term NB} remains secret\ +theorem Spy_not_see_NB [dest]: + assumes NB: "Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs" + "A \ bad" "B \ bad" + and evs: "evs \ ns_public" + shows "Nonce NB \ analz (spies evs)" + using evs NB evs +proof (induction rule: ns_public.induct) + case Fake + then show ?case by spy_analz +next + case NS2 + then show ?case + by (auto intro!: no_nonce_NS1_NS2) +qed auto -(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) -theorem Spy_not_see_NB [dest]: - "\Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ - \ Nonce NB \ analz (spies evs)" -apply (erule rev_mp) -apply (erule ns_public.induct, simp_all, spy_analz) -apply (blast intro: no_nonce_NS1_NS2)+ -done - - -(*Authentication for B: if he receives message 3 and has used NB - in message 2, then A has sent message 3.*) +text \Authentication for {term B}: if he receives message 3 and has used {term NB} + in message 2, then {term A} has sent message 3.\ lemma B_trusts_NS3_lemma [rule_format]: - "\A \ bad; B \ bad; evs \ ns_public\ \ - Crypt (pubEK B) (Nonce NB) \ parts (spies evs) \ - Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs \ - Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs" -by (erule ns_public.induct, auto) + "\evs \ ns_public; + Crypt (pubEK B) (Nonce NB) \ parts (spies evs); + Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; + A \ bad; B \ bad\ + \ Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs" +proof (induction rule: ns_public.induct) + case (NS3 evs3 A B NA B' NB) + then show ?case + by simp (blast intro: no_nonce_NS1_NS2) +qed auto theorem B_trusts_NS3: "\Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB, Agent B\) \ set evs; - Says A' B (Crypt (pubEK B) (Nonce NB)) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ + Says A' B (Crypt (pubEK B) (Nonce NB)) \ set evs; + A \ bad; B \ bad; evs \ ns_public\ \ Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs" -by (blast intro: B_trusts_NS3_lemma) + by (blast intro: B_trusts_NS3_lemma) -subsection\Overall guarantee for B\ + +subsection\Overall guarantee for {term B}\ -(*If NS3 has been sent and the nonce NB agrees with the nonce B joined with - NA, then A initiated the run using NA.*) +text \If NS3 has been sent and the nonce NB agrees with the nonce B joined with + NA, then A initiated the run using NA.\ theorem B_trusts_protocol: "\A \ bad; B \ bad; evs \ ns_public\ \ Crypt (pubEK B) (Nonce NB) \ parts (spies evs) \ diff -r eb30869e7228 -r efc220128637 src/HOL/Auth/NS_Public_Bad.thy --- a/src/HOL/Auth/NS_Public_Bad.thy Fri Oct 14 14:39:52 2022 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Oct 14 14:57:48 2022 +0100 @@ -1,78 +1,68 @@ (* Title: HOL/Auth/NS_Public_Bad.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge - -Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. -Flawed version, vulnerable to Lowe's attack. - -From page 260 of - Burrows, Abadi and Needham. A Logic of Authentication. - Proc. Royal Soc. 426 (1989) *) section\Verifying the Needham-Schroeder Public-Key Protocol\ +text \Flawed version, vulnerable to Lowe's attack. +From Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989), p. 260\ + theory NS_Public_Bad imports Public begin inductive_set ns_public :: "event list set" where - (*Initial trace is empty*) - Nil: "[] \ ns_public" - - (*The spy MAY say anything he CAN say. We do not expect him to - invent new nonces here, but he can also use NS1. Common to - all similar protocols.*) + Nil: "[] \ ns_public" + \ \Initial trace is empty\ | Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\ \ Says Spy B X # evsf \ ns_public" - - (*Alice initiates a protocol run, sending a nonce to Bob*) + \ \The spy can say almost anything.\ | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) # evs1 \ ns_public" - - (*Bob responds to Alice's message with a further nonce*) + \ \Alice initiates a protocol run, sending a nonce to Bob\ | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) # evs2 \ ns_public" - - (*Alice proves her existence by sending NB back to Bob.*) + \ \Bob responds to Alice's message with a further nonce\ | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs3; Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\ \ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \ ns_public" + \ \Alice proves her existence by sending @{term NB} back to Bob.\ declare knows_Spy_partsEs [elim] declare analz_into_parts [dest] declare Fake_parts_insert_in_Un [dest] -(*A "possibility property": there are traces that reach the end*) +text \A "possibility property": there are traces that reach the end\ lemma "\NB. \evs \ ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \ 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]) -by possibility + apply (intro exI bexI) + apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, THEN ns_public.NS3]) + by possibility -(**** Inductive proofs about ns_public ****) +subsection \Inductive proofs about @{term ns_public}\ (** Theorems of the form X \ parts (spies evs) imply that NOBODY sends messages containing X! **) -(*Spy never sees another agent's private key! (unless it's bad at start)*) +text \Spy never sees another agent's private key! (unless it's bad at start)\ lemma Spy_see_priEK [simp]: - "evs \ ns_public \ (Key (priEK A) \ parts (spies evs)) = (A \ bad)" -by (erule ns_public.induct, auto) + "evs \ ns_public \ (Key (priEK A) \ parts (spies evs)) = (A \ bad)" + by (erule ns_public.induct, auto) lemma Spy_analz_priEK [simp]: - "evs \ ns_public \ (Key (priEK A) \ analz (spies evs)) = (A \ bad)" -by auto + "evs \ ns_public \ (Key (priEK A) \ analz (spies evs)) = (A \ bad)" + by auto -(*** Authenticity properties obtained from NS2 ***) +subsection \Authenticity properties obtained from {term NS1}\ -(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce - is secret. (Honest users generate fresh nonces.)*) +text \It is impossible to re-use a nonce in both {term NS1} and {term NS2}, provided the nonce + is secret. (Honest users generate fresh nonces.)\ lemma no_nonce_NS1_NS2 [rule_format]: "evs \ ns_public \ Crypt (pubEK C) \NA', Nonce NA\ \ parts (spies evs) \ @@ -81,32 +71,42 @@ by (induct rule: ns_public.induct) (auto intro: analz_insertI) -(*Unicity for NS1: nonce NA identifies agents A and B*) +text \Unicity for {term NS1}: nonce {term NA} identifies agents {term A} and {term B}\ lemma unique_NA: - "\Crypt(pubEK B) \Nonce NA, Agent A \ \ parts(spies evs); - Crypt(pubEK B') \Nonce NA, Agent A'\ \ parts(spies evs); - Nonce NA \ analz (spies evs); evs \ ns_public\ - \ A=A' \ B=B'" -apply (erule rev_mp, erule rev_mp, erule rev_mp) -apply (erule ns_public.induct, auto intro: analz_insertI) -done + assumes NA: "Crypt(pubEK B) \Nonce NA, Agent A \ \ parts(spies evs)" + "Crypt(pubEK B') \Nonce NA, Agent A'\ \ parts(spies evs)" + "Nonce NA \ analz (spies evs)" + and evs: "evs \ ns_public" + shows "A=A' \ B=B'" + using evs NA + by (induction rule: ns_public.induct) (auto intro!: analz_insertI split: if_split_asm) -(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure - The major premise "Says A B ..." makes it a dest-rule, so we use - (erule rev_mp) rather than rule_format. *) +text \Secrecy: Spy does not see the nonce sent in msg {term NS1} if {term A} and {term B} are secure + The major premise "Says A B ..." makes it a dest-rule, hence the given assumption order. \ theorem Spy_not_see_NA: - "\Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ - \ Nonce NA \ analz (spies evs)" -apply (erule rev_mp) -apply (erule ns_public.induct, simp_all, spy_analz) -apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ -done + assumes NA: "Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs" + "A \ bad" "B \ bad" + and evs: "evs \ ns_public" + shows "Nonce NA \ analz (spies evs)" + using evs NA +proof (induction rule: ns_public.induct) + case (Fake evsf X B) + then show ?case + by spy_analz +next + case (NS2 evs2 NB A' B NA A) + then show ?case + by simp (metis Says_imp_analz_Spy analz_into_parts parts.simps unique_NA usedI) +next + case (NS3 evs3 A B NA B' NB) + then show ?case + by simp (meson Says_imp_analz_Spy analz_into_parts no_nonce_NS1_NS2) +qed auto -(*Authentication for A: if she receives message 2 and has used NA - to start a run, then B has sent message 2.*) +text \Authentication for {term A}: if she receives message 2 and has used {term NA} + to start a run, then {term B} has sent message 2.\ lemma A_trusts_NS2_lemma [rule_format]: "\A \ bad; B \ bad; evs \ ns_public\ \ Crypt (pubEK A) \Nonce NA, Nonce NB\ \ parts (spies evs) \ @@ -119,10 +119,10 @@ Says B' A (Crypt(pubEK A) \Nonce NA, Nonce NB\) \ set evs; A \ bad; B \ bad; evs \ ns_public\ \ Says B A (Crypt(pubEK A) \Nonce NA, Nonce NB\) \ set evs" -by (blast intro: A_trusts_NS2_lemma) + by (blast intro: A_trusts_NS2_lemma) -(*If the encrypted message appears then it originated with Alice in NS1*) +text \If the encrypted message appears then it originated with Alice in {term NS1}\ lemma B_trusts_NS1 [rule_format]: "evs \ ns_public \ Crypt (pubEK B) \Nonce NA, Agent A\ \ parts (spies evs) \ @@ -131,65 +131,72 @@ by (induction evs rule: ns_public.induct) (use analz_insertI in auto) - -(*** Authenticity properties obtained from NS2 ***) +subsection \Authenticity properties obtained from {term NS2}\ -(*Unicity for NS2: nonce NB identifies nonce NA and agent A - [proof closely follows that for unique_NA] *) +text \Unicity for {term NS2}: nonce {term NB} identifies nonce {term NA} and agent {term A} + [proof closely follows that for @{thm [source] unique_NA}]\ + lemma unique_NB [dest]: - "\Crypt(pubEK A) \Nonce NA, Nonce NB\ \ parts(spies evs); - Crypt(pubEK A') \Nonce NA', Nonce NB\ \ parts(spies evs); - Nonce NB \ analz (spies evs); evs \ ns_public\ - \ A=A' \ NA=NA'" -apply (erule rev_mp, erule rev_mp, erule rev_mp) -apply (erule ns_public.induct, simp_all) -(*Fake, NS2*) -apply (blast intro!: analz_insertI)+ -done + assumes NB: "Crypt(pubEK A) \Nonce NA, Nonce NB\ \ parts(spies evs)" + "Crypt(pubEK A') \Nonce NA', Nonce NB\ \ parts(spies evs)" + "Nonce NB \ analz (spies evs)" + and evs: "evs \ ns_public" + shows "A=A' \ NA=NA'" + using evs NB + by (induction rule: ns_public.induct) (auto intro!: analz_insertI split: if_split_asm) -(*NB remains secret PROVIDED Alice never responds with round 3*) +text \{term NB} remains secret \emph{provided} Alice never responds with round 3\ theorem Spy_not_see_NB [dest]: - "\Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs; - \C. Says A C (Crypt (pubEK C) (Nonce NB)) \ set evs; - A \ bad; B \ bad; evs \ ns_public\ - \ Nonce NB \ analz (spies evs)" -apply (erule rev_mp, erule rev_mp) -apply (erule ns_public.induct, simp_all, spy_analz) -apply (simp_all add: all_conj_distrib) (*speeds up the next step*) -apply (blast intro: no_nonce_NS1_NS2)+ -done + assumes NB: "Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs" + "\C. Says A C (Crypt (pubEK C) (Nonce NB)) \ set evs" + "A \ bad" "B \ bad" + and evs: "evs \ ns_public" + shows "Nonce NB \ analz (spies evs)" + using evs NB evs +proof (induction rule: ns_public.induct) + case Fake + then show ?case by spy_analz +next + case NS2 + then show ?case + by (auto intro!: no_nonce_NS1_NS2) +qed auto -(*Authentication for B: if he receives message 3 and has used NB - in message 2, then A has sent message 3--to somebody....*) - +text \Authentication for {term B}: if he receives message 3 and has used {term NB} + in message 2, then {term A} has sent message 3 (to somebody) \ lemma B_trusts_NS3_lemma [rule_format]: - "\A \ bad; B \ bad; evs \ ns_public\ - \ Crypt (pubEK B) (Nonce NB) \ parts (spies evs) \ - Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs \ - (\C. Says A C (Crypt (pubEK C) (Nonce NB)) \ set evs)" -apply (erule ns_public.induct, auto) -by (blast intro: no_nonce_NS1_NS2)+ + "\evs \ ns_public; + Crypt (pubEK B) (Nonce NB) \ parts (spies evs); + Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs; + A \ bad; B \ bad\ + \ \C. Says A C (Crypt (pubEK C) (Nonce NB)) \ set evs" +proof (induction rule: ns_public.induct) + case (NS3 evs3 A B NA B' NB) + then show ?case + by simp (blast intro: no_nonce_NS1_NS2) +qed auto theorem B_trusts_NS3: "\Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs; Says A' B (Crypt (pubEK B) (Nonce NB)) \ set evs; A \ bad; B \ bad; evs \ ns_public\ \ \C. Says A C (Crypt (pubEK C) (Nonce NB)) \ set evs" -by (blast intro: B_trusts_NS3_lemma) + by (blast intro: B_trusts_NS3_lemma) -(*Can we strengthen the secrecy theorem Spy_not_see_NB? NO*) -lemma "\A \ bad; B \ bad; evs \ ns_public\ - \ Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs - \ Nonce NB \ analz (spies evs)" -apply (erule ns_public.induct, simp_all, spy_analz) -(*NS1: by freshness*) +text \Can we strengthen the secrecy theorem @{thm[source]Spy_not_see_NB}? NO\ +lemma "\evs \ ns_public; + Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs; + A \ bad; B \ bad\ + \ Nonce NB \ analz (spies evs)" +apply (induction rule: ns_public.induct, simp_all, spy_analz) +(*{term NS1}: by freshness*) apply blast -(*NS2: by freshness and unicity of NB*) +(*{term NS2}: by freshness and unicity of {term NB}*) apply (blast intro: no_nonce_NS1_NS2) -(*NS3: unicity of NB identifies A and NA, but not B*) +(*{term NS3}: unicity of {term NB} identifies {term A} and {term NA}, but not {term B}*) apply clarify apply (frule_tac A' = A in Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto) diff -r eb30869e7228 -r efc220128637 src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Fri Oct 14 14:39:52 2022 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Fri Oct 14 14:57:48 2022 +0100 @@ -148,8 +148,8 @@ subsection\Towards Secrecy: Proofs Involving \<^term>\analz\\ -(*Describes the form of K and NA when the Server sends this message. Also - for Oops case.*) +text \Describes the form of K and NA when the Server sends this message. Also + for Oops case.\ lemma Says_Server_message_form: "\Says Server B \NA, X, Crypt (shrK B) \NB, Key K\\ \ set evs; evs \ otway\