[isabelle] about the proof of ns_public_bad protocol



    Hi:
    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?
                                                                       
                                                                       
                                                                 sincerely
                                                                       
                                                                       
                                                                    Jean
         





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