Re: [isabelle] about th proof of protocol



Jean,

On Wednesday 14 May 2008 05:18, jwang whu.edu.cn (jwang) wrote:
> 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.

I haven't looked at the Isabelle proof, but your e-mail suggests that "Say A B 
(Crypt(pubK B){Nonce NA,Agent A})</in>set [ ]" occurs as the premise of an 
implication "-->" in this subgoal.  Because this premise is false, the 
implication is trivially true.

Best,
Tjark





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