src/HOL/Auth/NS_Shared.thy
changeset 38617 f7b32911340b
parent 37936 1e4c5015a72e
child 38628 baf9f06601e4
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 20 16:28:53 2010 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Aug 20 16:44:48 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*}
     1.6  
     1.7 -theory NS_Shared imports Public begin
     1.8 +theory NS_Shared imports Sledgehammer2d(*###*) Public begin
     1.9  
    1.10  text{*
    1.11  From page 247 of
    1.12 @@ -311,6 +311,8 @@
    1.13        Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
    1.14        Says B A (Crypt K (Nonce NB)) \<in> set evs"
    1.15  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.16 +sledgehammer [atp = e, overlord] (Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
    1.17 +apply (metis Crypt_synth Fake_parts_insert_in_Un List.set.simps(2) Un_commute agent.simps(4) analz_insertI event.simps(1) insertE insert_iff knows_Spy_Says mem_def not_parts_not_analz parts_analz parts_synth sup1E)
    1.18  apply (analz_mono_contra, simp_all, blast)
    1.19  txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
    1.20      @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *}