1.1 --- a/src/HOL/Auth/Message.ML Wed Jul 21 15:20:26 1999 +0200
1.2 +++ b/src/HOL/Auth/Message.ML Wed Jul 21 15:22:11 1999 +0200
1.3 @@ -13,7 +13,6 @@
1.4 by (Blast_tac 1);
1.5 Addsimps [result()];
1.6
1.7 -AddIffs atomic.inject;
1.8 AddIffs msg.inject;
1.9
1.10 (*Equations hold because constructors are injective; cannot prove for all f*)
1.11 @@ -63,27 +62,27 @@
1.12 qed "keysFor_mono";
1.13
1.14 Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
1.15 -by (Blast_tac 1);
1.16 +by Auto_tac;
1.17 qed "keysFor_insert_Agent";
1.18
1.19 Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
1.20 -by (Blast_tac 1);
1.21 +by Auto_tac;
1.22 qed "keysFor_insert_Nonce";
1.23
1.24 Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
1.25 -by (Blast_tac 1);
1.26 +by Auto_tac;
1.27 qed "keysFor_insert_Number";
1.28
1.29 Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
1.30 -by (Blast_tac 1);
1.31 +by Auto_tac;
1.32 qed "keysFor_insert_Key";
1.33
1.34 Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
1.35 -by (Blast_tac 1);
1.36 +by Auto_tac;
1.37 qed "keysFor_insert_Hash";
1.38
1.39 Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
1.40 -by (Blast_tac 1);
1.41 +by Auto_tac;
1.42 qed "keysFor_insert_MPair";
1.43
1.44 Goalw [keysFor_def]
1.45 @@ -250,7 +249,7 @@
1.46 fun parts_tac i =
1.47 EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
1.48 etac parts.induct i,
1.49 - REPEAT (Blast_tac i)];
1.50 + Auto_tac];
1.51
1.52 Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
1.53 by (parts_tac 1);
1.54 @@ -308,7 +307,6 @@
1.55 (*In any message, there is an upper bound N on its greatest nonce.*)
1.56 Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
1.57 by (induct_tac "msg" 1);
1.58 -by (induct_tac "atomic" 1);
1.59 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
1.60 (*MPair case: blast_tac works out the necessary sum itself!*)
1.61 by (blast_tac (claset() addSEs [add_leE]) 2);
1.62 @@ -395,7 +393,7 @@
1.63 fun analz_tac i =
1.64 EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
1.65 etac analz.induct i,
1.66 - REPEAT (Blast_tac i)];
1.67 + Auto_tac];
1.68
1.69 Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
1.70 by (analz_tac 1);
1.71 @@ -442,7 +440,7 @@
1.72 \ insert (Crypt K X) (analz (insert X H))";
1.73 by (rtac subsetI 1);
1.74 by (eres_inst_tac [("xa","x")] analz.induct 1);
1.75 -by (ALLGOALS (Blast_tac));
1.76 +by Auto_tac;
1.77 val lemma1 = result();
1.78
1.79 Goal "Key (invKey K) : analz H ==> \
2.1 --- a/src/HOL/Auth/Message.thy Wed Jul 21 15:20:26 1999 +0200
2.2 +++ b/src/HOL/Auth/Message.thy Wed Jul 21 15:22:11 1999 +0200
2.3 @@ -28,36 +28,15 @@
2.4 datatype (*We allow any number of friendly agents*)
2.5 agent = Server | Friend nat | Spy
2.6
2.7 -
2.8 -(*Datatype msg is (awkwardly) split into two parts to avoid having freeness
2.9 - expressed using natural numbers.*)
2.10 -datatype
2.11 - atomic = AGENT agent (*Agent names*)
2.12 - | NUMBER nat (*Ordinary integers, timestamps, ...*)
2.13 - | NONCE nat (*Unguessable nonces*)
2.14 - | KEY key (*Crypto keys*)
2.15 -
2.16 datatype
2.17 - msg = Atomic atomic
2.18 + msg = Agent agent (*Agent names*)
2.19 + | Number nat (*Ordinary integers, timestamps, ...*)
2.20 + | Nonce nat (*Unguessable nonces*)
2.21 + | Key key (*Crypto keys*)
2.22 | Hash msg (*Hashing*)
2.23 | MPair msg msg (*Compound messages*)
2.24 | Crypt key msg (*Encryption, public- or shared-key*)
2.25
2.26 -(*These translations complete the illustion that "msg" has seven constructors*)
2.27 -syntax
2.28 - Agent :: agent => msg
2.29 - Number :: nat => msg
2.30 - Nonce :: nat => msg
2.31 - Key :: key => msg
2.32 -
2.33 -translations
2.34 - "Agent x" == "Atomic (AGENT x)"
2.35 - "Number x" == "Atomic (NUMBER x)"
2.36 - "Nonce x" == "Atomic (NONCE x)"
2.37 - "Nonce``x" == "Atomic `` (NONCE `` x)"
2.38 - "Key x" == "Atomic (KEY x)"
2.39 - "Key``x" == "Atomic `` (KEY `` x)"
2.40 -
2.41
2.42 (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
2.43 syntax
3.1 --- a/src/HOL/Auth/Recur.ML Wed Jul 21 15:20:26 1999 +0200
3.2 +++ b/src/HOL/Auth/Recur.ML Wed Jul 21 15:22:11 1999 +0200
3.3 @@ -368,8 +368,8 @@
3.4 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
3.5 by (ALLGOALS Clarify_tac);
3.6 by (blast_tac (claset() addSDs [resp_analz_insert]
3.7 - addIs [impOfSubs analz_subset_parts]) 2);
3.8 -by (blast_tac (claset() addSDs [respond_certificate]) 1);
3.9 + addIs [impOfSubs analz_subset_parts]) 3);
3.10 +by (blast_tac (claset() addSDs [respond_certificate]) 2);
3.11 by (Asm_full_simp_tac 1);
3.12 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
3.13 by (blast_tac
3.14 @@ -395,7 +395,7 @@
3.15 (*Fake*)
3.16 by (spy_analz_tac 2);
3.17 (*Base*)
3.18 -by (Blast_tac 1);
3.19 +by (Force_tac 1);
3.20 (*RA3 remains*)
3.21 by (simp_tac (simpset() addsimps [parts_insert_spies]) 1);
3.22 by (safe_tac (claset() delrules [impCE]));
4.1 --- a/src/HOL/Auth/TLS.ML Wed Jul 21 15:20:26 1999 +0200
4.2 +++ b/src/HOL/Auth/TLS.ML Wed Jul 21 15:22:11 1999 +0200
4.3 @@ -410,10 +410,10 @@
4.4 by (blast_tac (claset() addIs [parts_insertI]) 2);
4.5 (** LEVEL 6 **)
4.6 (*Oops*)
4.7 -by (Force_tac 6);
4.8 by (REPEAT
4.9 - (blast_tac (claset() addSDs [Notes_Crypt_parts_spies,
4.10 - Notes_master_imp_Crypt_PMS]) 1));
4.11 + (force_tac (claset() addSDs [Notes_Crypt_parts_spies,
4.12 + Notes_master_imp_Crypt_PMS],
4.13 + simpset()) 1));
4.14 val lemma = result();
4.15
4.16 Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \