src/HOL/Auth/TLS.thy
changeset 13507 febb8e5d2a9d
parent 11655 923e4d0d36d5
child 13922 75ae4244a596
     1.1 --- a/src/HOL/Auth/TLS.thy	Fri Aug 16 17:19:43 2002 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Sat Aug 17 14:55:08 2002 +0200
     1.3 @@ -318,9 +318,7 @@
     1.4                      [THEN tls.ClientHello, THEN tls.ServerHello,
     1.5                       THEN tls.Certificate, THEN tls.ClientKeyExch,
     1.6                       THEN tls.ClientFinished, THEN tls.ServerFinished,
     1.7 -                     THEN tls.ClientAccepts])
     1.8 -apply possibility
     1.9 -apply blast+
    1.10 +                     THEN tls.ClientAccepts], possibility, blast+)
    1.11  done
    1.12  
    1.13  
    1.14 @@ -333,9 +331,7 @@
    1.15                      [THEN tls.ClientHello, THEN tls.ServerHello,
    1.16                       THEN tls.Certificate, THEN tls.ClientKeyExch,
    1.17                       THEN tls.ServerFinished, THEN tls.ClientFinished, 
    1.18 -                     THEN tls.ServerAccepts])
    1.19 -apply possibility
    1.20 -apply blast+
    1.21 +                     THEN tls.ServerAccepts], possibility, blast+)
    1.22  done
    1.23  
    1.24  
    1.25 @@ -348,9 +344,7 @@
    1.26  apply (rule_tac [2] tls.Nil
    1.27                      [THEN tls.ClientHello, THEN tls.ServerHello,
    1.28                       THEN tls.Certificate, THEN tls.ClientKeyExch,
    1.29 -                     THEN tls.CertVerify])
    1.30 -apply possibility
    1.31 -apply blast+
    1.32 +                     THEN tls.CertVerify], possibility, blast+)
    1.33  done
    1.34  
    1.35  
    1.36 @@ -370,9 +364,7 @@
    1.37  apply (intro exI bexI)
    1.38  apply (rule_tac [2] tls.ClientHello
    1.39                      [THEN tls.ServerHello,
    1.40 -                     THEN tls.ServerResume, THEN tls.ClientResume])
    1.41 -apply possibility
    1.42 -apply blast+
    1.43 +                     THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+)
    1.44  done
    1.45  
    1.46  
    1.47 @@ -395,8 +387,7 @@
    1.48  (*Spy never sees a good agent's private key!*)
    1.49  lemma Spy_see_priK [simp]:
    1.50       "evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.51 -apply (erule tls.induct, force, simp_all)
    1.52 -apply blast
    1.53 +apply (erule tls.induct, force, simp_all, blast)
    1.54  done
    1.55  
    1.56  lemma Spy_analz_priK [simp]:
    1.57 @@ -415,8 +406,7 @@
    1.58  lemma certificate_valid:
    1.59      "[| certificate B KB \<in> parts (spies evs);  evs \<in> tls |] ==> KB = pubK B"
    1.60  apply (erule rev_mp)
    1.61 -apply (erule tls.induct, force, simp_all)
    1.62 -apply blast 
    1.63 +apply (erule tls.induct, force, simp_all, blast) 
    1.64  done
    1.65  
    1.66  lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
    1.67 @@ -467,8 +457,7 @@
    1.68           evs \<in> tls;  A \<notin> bad |]
    1.69        ==> Says A B X \<in> set evs"
    1.70  apply (erule rev_mp, erule ssubst)
    1.71 -apply (erule tls.induct, force, simp_all)
    1.72 -apply blast
    1.73 +apply (erule tls.induct, force, simp_all, blast)
    1.74  done
    1.75  
    1.76  (*Final version: B checks X using the distributed KA instead of priK A*)
    1.77 @@ -487,8 +476,7 @@
    1.78           evs \<in> tls;  A \<notin> bad |]
    1.79        ==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
    1.80  apply (erule rev_mp)
    1.81 -apply (erule tls.induct, force, simp_all)
    1.82 -apply blast
    1.83 +apply (erule tls.induct, force, simp_all, blast)
    1.84  done
    1.85  
    1.86  (*Final version using the distributed KA instead of priK A*)