[isabelle] about th proof of protocol

  I 'm  studing the proof procedure of Ns_Public_Bad protocol in Isabelle.How  some theorem  are proved  in NIL([] trace) puzzled me greatly.For example ,theorem Spy_not see_NA.When applying "erule ns_public.induct", five subgoals will be given.The first subgoal is "[A  /<not in> bad;B /<not in> bad]=>Say A B (Crypt(pubK B){Nonce NA,Agent A})</in>set [ ]-->Nonce  NA /<not in> a nalz(knows  Spy []).I can't understand  how the subgoal is proved.I think the first subgoal is not tenable because "Say A B (Crypt(pubK B){Nonce NA,Agent A})" impossiblely belongs to [] trace.
    Wish for your  answer.
                                                                          & nbsp;                                                                         &n bsp;                                       Jean

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