# HG changeset patch # User paulson # Date 851073926 -3600 # Node ID 9c4444bfd44ed85e45576941e1ab999f8f7d4452 # Parent 92f43ed48935528345fd520ed37ce7b7407ae893 Simplification and generalization of the guarantees. Nonces are not required for binding, merely for freshness. diff -r 92f43ed48935 -r 9c4444bfd44e src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Fri Dec 20 10:23:48 1996 +0100 +++ b/src/HOL/Auth/Recur.ML Fri Dec 20 10:25:26 1996 +0100 @@ -406,6 +406,8 @@ (** The Nonce NA uniquely identifies A's message. This theorem applies to rounds RA1 and RA2! + + Unicity is not used in other proofs but is desirable in its own right. **) goal thy @@ -464,6 +466,7 @@ ***) (*The response never contains Hashes*) +(*NEEDED????????????????*) goal thy "!!evs. (j,PB,RB) : respond i \ \ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \ @@ -607,9 +610,8 @@ goal thy - "!!evs. [| A ~: lost; A' ~: lost; \ -\ evs : recur lost |] \ -\ ==> Says Server B RB : set_of_list evs --> \ + "!!evs. [| A ~: lost; A' ~: lost; evs : recur lost |] \ +\ ==> Says Server B RB : set_of_list evs --> \ \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac recur.induct 1); @@ -638,10 +640,10 @@ goal thy - "!!evs. [| Says Server B RB : set_of_list evs; \ + "!!evs. [| Says Server B RB : set_of_list evs; \ \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB}; \ -\ C ~: {A,A',Server}; \ -\ A ~: lost; A' ~: lost; evs : recur lost |] \ +\ C ~: {A,A',Server}; \ +\ A ~: lost; A' ~: lost; evs : recur lost |] \ \ ==> Key K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); @@ -652,6 +654,7 @@ (**** Authenticity properties for Agents ****) +(*NEEDED????????????????*) (*Only RA1 or RA2 can have caused such a part of a message to appear.*) goal thy "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \ @@ -665,7 +668,7 @@ (*RA3*) by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2); (*RA2*) -by ((REPEAT o CHANGED) (*Push in XA*) +by ((REPEAT o CHANGED) (*Push in XA--for more simplification*) (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1)); by (best_tac (!claset addSEs partsEs addDs [parts_cut] @@ -673,6 +676,7 @@ qed_spec_mp "Hash_auth_sender"; +(*NEEDED????????????????*) goal thy "!!i. {|Hash {|Key (shrK Server), M|}, M|} : responses i ==> R"; be setup_induction 1; be responses.induct 1; @@ -688,51 +692,37 @@ **) -(*Crucial property: If the encrypted message appears, and A has used NA - in a run, then it originated with the Server!*) +(*Encrypted messages can only originate with the Server.*) goal thy - "!!evs. [| A ~: lost; A ~= Spy; evs : recur lost |] \ -\ ==> Crypt (shrK A) {|Key K, Agent A', NA|} : parts (sees lost Spy evs) \ -\ --> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \ -\ Agent A, Agent B, NA, P|} \ -\ : set_of_list evs \ -\ --> (EX C RC. Says Server C RC : set_of_list evs & \ -\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC})"; + "!!evs. [| A ~: lost; A ~= Spy; evs : recur lost |] \ +\ ==> Crypt (shrK A) Y : parts (sees lost Spy evs) \ +\ --> (EX C RC. Says Server C RC : set_of_list evs & \ +\ Crypt (shrK A) Y : parts {RC})"; by (parts_induct_tac 1); (*RA4*) -by (best_tac (!claset addSEs [MPair_parts] - addSDs [Hash_auth_sender] - addSIs [disjI2]) 4); -(*RA1: it cannot be a new Nonce, contradiction.*) -by (fast_tac (!claset delrules [impCE] - addSEs [nonce_not_seen_now, MPair_parts] - addDs [parts.Body]) 1); +by (Fast_tac 4); +(*RA3*) +by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3 + THEN Fast_tac 3); +(*RA1*) +by (Fast_tac 1); (*RA2: it cannot be a new Nonce, contradiction.*) -by ((REPEAT o CHANGED) (*Push in XA*) +by ((REPEAT o CHANGED) (*Push in XA--for more simplification*) (res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1)); by (deepen_tac (!claset delrules [impCE] addSIs [disjI2] - addSEs [MPair_parts] + addSEs [MPair_parts] addDs [parts_cut, parts.Body] addss (!simpset)) 0 1); -(*RA3*) (** LEVEL 5 **) -by (REPEAT (safe_step_tac (!claset addSEs [responses_no_Hash_Server] - delrules [impCE]) 1)); -by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 1); -by (Fast_tac 1); qed_spec_mp "Crypt_imp_Server_msg"; -(*Corollary: if A receives B's message and the nonce NA agrees - then the key really did come from the Server!*) +(*Corollary: if A receives B's message then the key came from the Server*) goal thy "!!evs. [| Says B' A RA : set_of_list evs; \ -\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \ -\ Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \ -\ Agent A, Agent B, NA, P|} \ -\ : set_of_list evs; \ +\ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \ \ A ~: lost; A ~= Spy; evs : recur lost |] \ -\ ==> EX C RC. Says Server C RC : set_of_list evs & \ +\ ==> EX C RC. Says Server C RC : set_of_list evs & \ \ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC}"; by (best_tac (!claset addSIs [Crypt_imp_Server_msg] addDs [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)] @@ -740,14 +730,11 @@ qed "Agent_trust"; -(*Overall guarantee: if A receives B's message and the nonce NA agrees - then the only other agent who knows the key is B.*) +(*Overall guarantee: if A receives a certificant mentioning A' + then the only other agent who knows the key is A'.*) goal thy "!!evs. [| Says B' A RA : set_of_list evs; \ \ Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA}; \ -\ Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|}, \ -\ Agent A, Agent B, NA, P|} \ -\ : set_of_list evs; \ \ C ~: {A,A',Server}; \ \ A ~: lost; A' ~: lost; A ~= Spy; evs : recur lost |] \ \ ==> Key K ~: analz (sees lost C evs)";