diff -r c6c6c2bc6fe8 -r c71657bbdbc0 src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Metis_Examples/Message.thy Mon Jun 06 20:36:35 2011 +0200 @@ -1,10 +1,12 @@ (* Title: HOL/Metis_Examples/Message.thy - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen -Testing Metis. +Metis example featuring message authentication. *) +header {* Metis Example Featuring Message Authentication *} + theory Message imports Main begin @@ -135,7 +137,7 @@ lemma keysFor_insert_MPair [simp]: "keysFor (insert {|X,Y|} H) = keysFor H" by (unfold keysFor_def, auto) -lemma keysFor_insert_Crypt [simp]: +lemma keysFor_insert_Crypt [simp]: "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)" by (unfold keysFor_def, auto) @@ -149,13 +151,13 @@ subsection{*Inductive relation "parts"*} lemma MPair_parts: - "[| {|X,Y|} \ parts H; + "[| {|X,Y|} \ parts H; [| X \ parts H; Y \ parts H |] ==> P |] ==> P" -by (blast dest: parts.Fst parts.Snd) +by (blast dest: parts.Fst parts.Snd) declare MPair_parts [elim!] parts.Body [dest!] text{*NB These two rules are UNSAFE in the formal sense, as they discard the - compound message. They work well on THIS FILE. + compound message. They work well on THIS FILE. @{text MPair_parts} is left as SAFE because it speeds up proofs. The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*} @@ -218,9 +220,9 @@ NOTE: the UN versions are no longer used!*} -text{*This allows @{text blast} to simplify occurrences of +text{*This allows @{text blast} to simplify occurrences of @{term "parts(G\H)"} in the assumption.*} -lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] +lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] declare in_parts_UnE [elim!] lemma parts_insert_subset: "insert X (parts H) \ parts(insert X H)" @@ -235,13 +237,13 @@ by blast lemma parts_subset_iff [simp]: "(parts G \ parts H) = (G \ parts H)" -apply (rule iffI) +apply (rule iffI) apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing) apply (metis parts_idem parts_mono) done lemma parts_trans: "[| X\ parts G; G \ parts H |] ==> X\ parts H" -by (blast dest: parts_mono); +by (blast dest: parts_mono); lemma parts_cut: "[|Y\ parts (insert X G); X\ parts H|] ==> Y\ parts(G \ H)" by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI) @@ -254,36 +256,36 @@ lemma parts_insert_Agent [simp]: "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Nonce [simp]: "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Number [simp]: "parts (insert (Number N) H) = insert (Number N) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Key [simp]: "parts (insert (Key K) H) = insert (Key K) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Hash [simp]: "parts (insert (Hash X) H) = insert (Hash X) (parts H)" -apply (rule parts_insert_eq_I) -apply (erule parts.induct, auto) +apply (rule parts_insert_eq_I) +apply (erule parts.induct, auto) done lemma parts_insert_Crypt [simp]: - "parts (insert (Crypt K X) H) = + "parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H))" apply (rule equalityI) apply (rule subsetI) @@ -292,7 +294,7 @@ done lemma parts_insert_MPair [simp]: - "parts (insert {|X,Y|} H) = + "parts (insert {|X,Y|} H) = insert {|X,Y|} (parts (insert X (insert Y H)))" apply (rule equalityI) apply (rule subsetI) @@ -306,7 +308,7 @@ done lemma msg_Nonce_supply: "\N. \n. N\n --> Nonce n \ parts {msg}" -apply (induct_tac "msg") +apply (induct_tac "msg") apply (simp_all add: parts_insert2) apply (metis Suc_n_not_le_n) apply (metis le_trans linorder_linear) @@ -325,21 +327,21 @@ Inj [intro,simp] : "X \ H ==> X \ analz H" | Fst: "{|X,Y|} \ analz H ==> X \ analz H" | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - | Decrypt [dest]: + | Decrypt [dest]: "[|Crypt K X \ analz H; Key(invKey K): analz H|] ==> X \ analz H" text{*Monotonicity; Lemma 1 of Lowe's paper*} lemma analz_mono: "G\H ==> analz(G) \ analz(H)" apply auto -apply (erule analz.induct) -apply (auto dest: analz.Fst analz.Snd) +apply (erule analz.induct) +apply (auto dest: analz.Fst analz.Snd) done text{*Making it safe speeds up proofs*} lemma MPair_analz [elim!]: - "[| {|X,Y|} \ analz H; - [| X \ analz H; Y \ analz H |] ==> P + "[| {|X,Y|} \ analz H; + [| X \ analz H; Y \ analz H |] ==> P |] ==> P" by (blast dest: analz.Fst analz.Snd) @@ -376,7 +378,7 @@ apply (erule analz.induct, blast+) done -text{*Converse fails: we can analz more from the union than from the +text{*Converse fails: we can analz more from the union than from the separate parts, as a key in one might decrypt a message in the other*} lemma analz_Un: "analz(G) \ analz(H) \ analz(G \ H)" by (intro Un_least analz_mono Un_upper1 Un_upper2) @@ -390,39 +392,39 @@ lemma analz_insert_Agent [simp]: "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_Nonce [simp]: "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_Number [simp]: "analz (insert (Number N) H) = insert (Number N) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_Hash [simp]: "analz (insert (Hash X) H) = insert (Hash X) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done text{*Can only pull out Keys if they are not needed to decrypt the rest*} -lemma analz_insert_Key [simp]: - "K \ keysFor (analz H) ==> +lemma analz_insert_Key [simp]: + "K \ keysFor (analz H) ==> analz (insert (Key K) H) = insert (Key K) (analz H)" apply (unfold keysFor_def) -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done lemma analz_insert_MPair [simp]: - "analz (insert {|X,Y|} H) = + "analz (insert {|X,Y|} H) = insert {|X,Y|} (analz (insert X (insert Y H)))" apply (rule equalityI) apply (rule subsetI) @@ -433,22 +435,22 @@ text{*Can pull out enCrypted message if the Key is not known*} lemma analz_insert_Crypt: - "Key (invKey K) \ analz H + "Key (invKey K) \ analz H ==> analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)" -apply (rule analz_insert_eq_I) -apply (erule analz.induct, auto) +apply (rule analz_insert_eq_I) +apply (erule analz.induct, auto) done -lemma lemma1: "Key (invKey K) \ analz H ==> - analz (insert (Crypt K X) H) \ - insert (Crypt K X) (analz (insert X H))" +lemma lemma1: "Key (invKey K) \ analz H ==> + analz (insert (Crypt K X) H) \ + insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) apply (erule_tac x = x in analz.induct, auto) done -lemma lemma2: "Key (invKey K) \ analz H ==> - insert (Crypt K X) (analz (insert X H)) \ +lemma lemma2: "Key (invKey K) \ analz H ==> + insert (Crypt K X) (analz (insert X H)) \ analz (insert (Crypt K X) H)" apply auto apply (erule_tac x = x in analz.induct, auto) @@ -456,26 +458,26 @@ done lemma analz_insert_Decrypt: - "Key (invKey K) \ analz H ==> - analz (insert (Crypt K X) H) = + "Key (invKey K) \ analz H ==> + analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H))" by (intro equalityI lemma1 lemma2) text{*Case analysis: either the message is secure, or it is not! Effective, but can cause subgoals to blow up! Use with @{text "split_if"}; apparently @{text "split_tac"} does not cope with patterns such as @{term"analz (insert -(Crypt K X) H)"} *} +(Crypt K X) H)"} *} lemma analz_Crypt_if [simp]: - "analz (insert (Crypt K X) H) = - (if (Key (invKey K) \ analz H) - then insert (Crypt K X) (analz (insert X H)) + "analz (insert (Crypt K X) H) = + (if (Key (invKey K) \ analz H) + then insert (Crypt K X) (analz (insert X H)) else insert (Crypt K X) (analz H))" by (simp add: analz_insert_Crypt analz_insert_Decrypt) text{*This rule supposes "for the sake of argument" that we have the key.*} lemma analz_insert_Crypt_subset: - "analz (insert (Crypt K X) H) \ + "analz (insert (Crypt K X) H) \ insert (Crypt K X) (analz (insert X H))" apply (rule subsetI) apply (erule analz.induct, auto) @@ -498,8 +500,8 @@ lemma analz_subset_iff [simp]: "(analz G \ analz H) = (G \ analz H)" apply (rule iffI) -apply (iprover intro: subset_trans analz_increasing) -apply (frule analz_mono, simp) +apply (iprover intro: subset_trans analz_increasing) +apply (frule analz_mono, simp) done lemma analz_trans: "[| X\ analz G; G \ analz H |] ==> X\ analz H" @@ -525,7 +527,7 @@ text{*A congruence rule for "analz" *} lemma analz_subset_cong: - "[| analz G \ analz G'; analz H \ analz H' |] + "[| analz G \ analz G'; analz H \ analz H' |] ==> analz (G \ H) \ analz (G' \ H')" apply simp apply (metis Un_absorb2 Un_commute Un_subset_iff Un_upper1 Un_upper2 analz_mono) @@ -533,9 +535,9 @@ lemma analz_cong: - "[| analz G = analz G'; analz H = analz H' + "[| analz G = analz G'; analz H = analz H' |] ==> analz (G \ H) = analz (G' \ H')" -by (intro equalityI analz_subset_cong, simp_all) +by (intro equalityI analz_subset_cong, simp_all) lemma analz_insert_cong: "analz H = analz H' ==> analz(insert X H) = analz(insert X H')" @@ -579,9 +581,9 @@ text{*Monotonicity*} lemma synth_mono: "G\H ==> synth(G) \ synth(H)" - by (auto, erule synth.induct, auto) + by (auto, erule synth.induct, auto) -text{*NO @{text Agent_synth}, as any Agent name can be synthesized. +text{*NO @{text Agent_synth}, as any Agent name can be synthesized. The same holds for @{term Number}*} inductive_cases Nonce_synth [elim!]: "Nonce n \ synth H" inductive_cases Key_synth [elim!]: "Key K \ synth H" @@ -595,7 +597,7 @@ subsubsection{*Unions *} -text{*Converse fails: we can synth more from the union than from the +text{*Converse fails: we can synth more from the union than from the separate parts, building a compound message using elements of each.*} lemma synth_Un: "synth(G) \ synth(H) \ synth(G \ H)" by (intro Un_least synth_mono Un_upper1 Un_upper2) @@ -613,8 +615,8 @@ lemma synth_subset_iff [simp]: "(synth G \ synth H) = (G \ synth H)" apply (rule iffI) -apply (iprover intro: subset_trans synth_increasing) -apply (frule synth_mono, simp add: synth_idem) +apply (iprover intro: subset_trans synth_increasing) +apply (frule synth_mono, simp add: synth_idem) done lemma synth_trans: "[| X\ synth G; G \ synth H |] ==> X\ synth H" @@ -644,7 +646,7 @@ by blast -lemma keysFor_synth [simp]: +lemma keysFor_synth [simp]: "keysFor (synth H) = keysFor H \ invKey`{K. Key K \ H}" by (unfold keysFor_def, blast) @@ -706,7 +708,7 @@ qed lemma Fake_parts_insert: - "X \ synth (analz H) ==> + "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" proof - assume A1: "X \ synth (analz H)" @@ -735,11 +737,11 @@ qed lemma Fake_parts_insert_in_Un: - "[|Z \ parts (insert X H); X: synth (analz H)|] + "[|Z \ parts (insert X H); X: synth (analz H)|] ==> Z \ synth (analz H) \ parts H"; by (blast dest: Fake_parts_insert [THEN subsetD, dest]) -declare analz_mono [intro] synth_mono [intro] +declare analz_mono [intro] synth_mono [intro] lemma Fake_analz_insert: "X \ synth (analz G) ==> @@ -748,7 +750,7 @@ analz_mono analz_synth_Un insert_absorb) lemma Fake_analz_insert_simpler: - "X \ synth (analz G) ==> + "X \ synth (analz G) ==> analz (insert X H) \ synth (analz G) \ analz (G \ H)" apply (rule subsetI) apply (subgoal_tac "x \ analz (synth (analz G) \ H) ")