[isabelle] about the proof of ns_public_bad protocol

    Now,I'm  studing the proof process of Ns_Bublic_Bad.thy in the  path
"src/HOl/Auth/Ns_Punlic_Bad.thy".I run the Ns_Bublic_Bad.thy in ISABELLE
and analyse
the proof scripts of Ns_Punlic_Bad protocol.But I could not understand
the proof process of  the theorem   Spy_not_see_NA and
A_trusts_NS2_lemma.Applying erule ns_public.induct,then five subgoals
were given,but how  were the five subgoals  proved?why Ba belong to
"bad"  in evs1,evs3 and Aa belong to "bad 'in  evs2?

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.