# HG changeset patch # User paulson # Date 867772776 -7200 # Node ID 6988394a600871ecec151e5bc6977e6d2a25cb3b # Parent ef918a90f9bf18ddd1d393a74bad61671fa9989d Tidying; also simplified the lemma Says_Server_not diff -r ef918a90f9bf -r 6988394a6008 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Tue Jul 01 17:42:36 1997 +0200 +++ b/src/HOL/Auth/Recur.ML Tue Jul 01 17:59:36 1997 +0200 @@ -21,8 +21,8 @@ (*Simplest case: Alice goes directly to the server*) goal thy - "!!A. A ~= Server \ -\ ==> EX K NA. EX evs: recur lost. \ + "!!A. A ~= Server \ +\ ==> EX K NA. EX evs: recur lost. \ \ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ \ Agent Server|} : set evs"; by (REPEAT (resolve_tac [exI,bexI] 1)); @@ -34,8 +34,8 @@ (*Case two: Alice, Bob and the server*) goal thy - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ -\ ==> EX K. EX NA. EX evs: recur lost. \ + "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX K. EX NA. EX evs: recur lost. \ \ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ \ Agent Server|} : set evs"; by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); @@ -54,8 +54,8 @@ TOO SLOW to run every time! goal thy "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \ -\ ==> EX K. EX NA. EX evs: recur lost. \ -\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ +\ ==> EX K. EX NA. EX evs: recur lost. \ +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ \ Agent Server|} : set evs"; by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); by (REPEAT (eresolve_tac [exE, conjE] 1)); @@ -324,14 +324,14 @@ by (ALLGOALS (expand_case_tac "NA = ?y")); by (REPEAT_FIRST (ares_tac [exI])); by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] - addSEs sees_Spy_partsEs) 1)); + addSEs sees_Spy_partsEs) 1)); val lemma = result(); goalw thy [HPair_def] - "!!evs.[| Hash[Key(shrK A)] {|Agent A,B,NA,P|} : parts (sees lost Spy evs); \ -\ Hash[Key(shrK A)] {|Agent A,B',NA,P'|} : parts (sees lost Spy evs);\ -\ evs : recur lost; A ~: lost |] \ -\ ==> B=B' & P=P'"; + "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts(sees lost Spy evs); \ +\ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts(sees lost Spy evs); \ +\ evs : recur lost; A ~: lost |] \ +\ ==> B=B' & P=P'"; by (REPEAT (eresolve_tac partsEs 1)); by (prove_unique_tac lemma 1); qed "unique_NA"; @@ -358,7 +358,7 @@ \ ALL K KK. KK <= Compl (range shrK) --> \ \ (Key K : analz (Key``KK Un H)) = \ \ (K : KK | Key K : analz H) |] \ -\ ==> (Key K : analz (insert RB H)) --> \ +\ ==> (Key K : analz (insert RB H)) --> \ \ (Key K : parts{RB} | Key K : analz H)"; by (etac responses.induct 1); by (ALLGOALS @@ -377,9 +377,8 @@ (*The Server does not send such messages. This theorem lets us avoid assuming B~=Server in RA4.*) goal thy - "!!evs. evs : recur lost \ -\ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \ -\ ~: set evs"; + "!!evs. evs : recur lost \ +\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs"; by (etac recur.induct 1); by (etac (respond.induct) 5); by (Auto_tac());