Re: [isabelle] about th proof of protocol

Trivially, analz(knows Spy []) is empty (see definitions).

Tjark Weber wrote:

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


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