src/HOL/Auth/TLS.ML
changeset 7057 b9ddbb925939
parent 6915 4ab8e31a8421
child 8054 2ce57ef2a4aa
equal deleted inserted replaced
7056:522a7013d7df 7057:b9ddbb925939
   408 by (Blast_tac 3);
   408 by (Blast_tac 3);
   409 (*Fake*)
   409 (*Fake*)
   410 by (blast_tac (claset() addIs [parts_insertI]) 2);
   410 by (blast_tac (claset() addIs [parts_insertI]) 2);
   411 (** LEVEL 6 **)
   411 (** LEVEL 6 **)
   412 (*Oops*)
   412 (*Oops*)
   413 by (Force_tac 6);
       
   414 by (REPEAT 
   413 by (REPEAT 
   415     (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
   414     (force_tac (claset() addSDs [Notes_Crypt_parts_spies, 
   416 				 Notes_master_imp_Crypt_PMS]) 1));
   415 				 Notes_master_imp_Crypt_PMS],
       
   416 		simpset()) 1));
   417 val lemma = result();
   417 val lemma = result();
   418 
   418 
   419 Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \
   419 Goal "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) : parts (spies evs); \
   420 \        evs : tls |]             \
   420 \        evs : tls |]             \
   421 \     ==> Nonce PMS : parts (spies evs)";
   421 \     ==> Nonce PMS : parts (spies evs)";