# HG changeset patch # User paulson # Date 866712277 -7200 # Node ID 6b17f82bbf01a2615a4b18b1701c27f6f9147e8d # Parent 8a79e27ac53b039f28f2f978fd1283bcbc421e8c New comments; a tidied proof diff -r 8a79e27ac53b -r 6b17f82bbf01 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Thu Jun 19 11:23:31 1997 +0200 +++ b/src/HOL/Auth/Message.ML Thu Jun 19 11:24:37 1997 +0200 @@ -405,8 +405,7 @@ by (Auto_tac()); by (eres_inst_tac [("za","x")] analz.induct 1); by (Auto_tac()); -by (blast_tac (!claset addIs [subset_insertI RS analz_mono RS subsetD, - analz.Decrypt]) 1); +by (blast_tac (!claset addIs [analz_insertI, analz.Decrypt]) 1); val lemma2 = result(); goal thy "!!H. Key (invKey K) : analz H ==> \ @@ -477,6 +476,9 @@ "!!H. Y: analz (insert X H) ==> X: analz H --> Y: analz H" *) +(*This rewrite rule helps in the simplification of messages that involve + the forwarding of unknown components (X). Without it, removing occurrences + of X can be very complicated. *) goal thy "!!H. X: analz H ==> analz (insert X H) = analz H"; by (blast_tac (!claset addIs [analz_cut, analz_insertI]) 1); qed "analz_insert_eq"; @@ -839,7 +841,8 @@ impOfSubs Fake_parts_insert] THEN' eresolve_tac [asm_rl, synth.Inj]; -(*Analysis of Fake cases and of messages that forward unknown parts. +(*Analysis of Fake cases. Also works for messages that forward unknown parts, + but this application is no longer necessary if analz_insert_eq is used. Abstraction over i is ESSENTIAL: it delays the dereferencing of claset DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) fun spy_analz_tac i =