src/HOL/Auth/Message.ML
changeset 7057 b9ddbb925939
parent 6915 4ab8e31a8421
child 8054 2ce57ef2a4aa
equal deleted inserted replaced
7056:522a7013d7df 7057:b9ddbb925939
    11 (*Eliminates a commonly-occurring expression*)
    11 (*Eliminates a commonly-occurring expression*)
    12 goal HOL.thy "~ (ALL x. x~=y)";
    12 goal HOL.thy "~ (ALL x. x~=y)";
    13 by (Blast_tac 1);
    13 by (Blast_tac 1);
    14 Addsimps [result()];
    14 Addsimps [result()];
    15 
    15 
    16 AddIffs atomic.inject;
       
    17 AddIffs msg.inject;
    16 AddIffs msg.inject;
    18 
    17 
    19 (*Equations hold because constructors are injective; cannot prove for all f*)
    18 (*Equations hold because constructors are injective; cannot prove for all f*)
    20 Goal "(Friend x : Friend``A) = (x:A)";
    19 Goal "(Friend x : Friend``A) = (x:A)";
    21 by Auto_tac;
    20 by Auto_tac;
    61 Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)";
    60 Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)";
    62 by (Blast_tac 1);
    61 by (Blast_tac 1);
    63 qed "keysFor_mono";
    62 qed "keysFor_mono";
    64 
    63 
    65 Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    64 Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    66 by (Blast_tac 1);
    65 by Auto_tac;
    67 qed "keysFor_insert_Agent";
    66 qed "keysFor_insert_Agent";
    68 
    67 
    69 Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    68 Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    70 by (Blast_tac 1);
    69 by Auto_tac;
    71 qed "keysFor_insert_Nonce";
    70 qed "keysFor_insert_Nonce";
    72 
    71 
    73 Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
    72 Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
    74 by (Blast_tac 1);
    73 by Auto_tac;
    75 qed "keysFor_insert_Number";
    74 qed "keysFor_insert_Number";
    76 
    75 
    77 Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    76 Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    78 by (Blast_tac 1);
    77 by Auto_tac;
    79 qed "keysFor_insert_Key";
    78 qed "keysFor_insert_Key";
    80 
    79 
    81 Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    80 Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    82 by (Blast_tac 1);
    81 by Auto_tac;
    83 qed "keysFor_insert_Hash";
    82 qed "keysFor_insert_Hash";
    84 
    83 
    85 Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    84 Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    86 by (Blast_tac 1);
    85 by Auto_tac;
    87 qed "keysFor_insert_MPair";
    86 qed "keysFor_insert_MPair";
    88 
    87 
    89 Goalw [keysFor_def]
    88 Goalw [keysFor_def]
    90     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
    89     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
    91 by Auto_tac;
    90 by Auto_tac;
   248 (** Rewrite rules for pulling out atomic messages **)
   247 (** Rewrite rules for pulling out atomic messages **)
   249 
   248 
   250 fun parts_tac i =
   249 fun parts_tac i =
   251   EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
   250   EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
   252          etac parts.induct i,
   251          etac parts.induct i,
   253          REPEAT (Blast_tac i)];
   252          Auto_tac];
   254 
   253 
   255 Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   254 Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   256 by (parts_tac 1);
   255 by (parts_tac 1);
   257 qed "parts_insert_Agent";
   256 qed "parts_insert_Agent";
   258 
   257 
   306 
   305 
   307 
   306 
   308 (*In any message, there is an upper bound N on its greatest nonce.*)
   307 (*In any message, there is an upper bound N on its greatest nonce.*)
   309 Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
   308 Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
   310 by (induct_tac "msg" 1);
   309 by (induct_tac "msg" 1);
   311 by (induct_tac "atomic" 1);
       
   312 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
   310 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
   313 (*MPair case: blast_tac works out the necessary sum itself!*)
   311 (*MPair case: blast_tac works out the necessary sum itself!*)
   314 by (blast_tac (claset() addSEs [add_leE]) 2);
   312 by (blast_tac (claset() addSEs [add_leE]) 2);
   315 (*Nonce case*)
   313 (*Nonce case*)
   316 by (res_inst_tac [("x","N + Suc nat")] exI 1);
   314 by (res_inst_tac [("x","N + Suc nat")] exI 1);
   393 (** Rewrite rules for pulling out atomic messages **)
   391 (** Rewrite rules for pulling out atomic messages **)
   394 
   392 
   395 fun analz_tac i =
   393 fun analz_tac i =
   396   EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   394   EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   397          etac analz.induct i,
   395          etac analz.induct i,
   398          REPEAT (Blast_tac i)];
   396          Auto_tac];
   399 
   397 
   400 Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   398 Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   401 by (analz_tac 1);
   399 by (analz_tac 1);
   402 qed "analz_insert_Agent";
   400 qed "analz_insert_Agent";
   403 
   401 
   440 Goal "Key (invKey K) : analz H ==>  \
   438 Goal "Key (invKey K) : analz H ==>  \
   441 \              analz (insert (Crypt K X) H) <= \
   439 \              analz (insert (Crypt K X) H) <= \
   442 \              insert (Crypt K X) (analz (insert X H))";
   440 \              insert (Crypt K X) (analz (insert X H))";
   443 by (rtac subsetI 1);
   441 by (rtac subsetI 1);
   444 by (eres_inst_tac [("xa","x")] analz.induct 1);
   442 by (eres_inst_tac [("xa","x")] analz.induct 1);
   445 by (ALLGOALS (Blast_tac));
   443 by Auto_tac;
   446 val lemma1 = result();
   444 val lemma1 = result();
   447 
   445 
   448 Goal "Key (invKey K) : analz H ==>  \
   446 Goal "Key (invKey K) : analz H ==>  \
   449 \              insert (Crypt K X) (analz (insert X H)) <= \
   447 \              insert (Crypt K X) (analz (insert X H)) <= \
   450 \              analz (insert (Crypt K X) H)";
   448 \              analz (insert (Crypt K X) H)";