Re: [isabelle] about th proof of protocol




Another good exercise to understand why things happens in the proofs is to enable the Traces (simplifier and unification) in Isabelle.

This doubt you had is easy to grasp from the simplifier trace.


Jean

Tjark Weber escreveu:
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.