*To*: Tjark Weber <tjark.weber at gmx.de>*Subject*: Re: [isabelle] about th proof of protocol*From*: Cristiano Longo <cristiano.longo at tvblob.com>*Date*: Thu, 15 May 2008 12:20:29 +0200*Cc*: jwang at whu.edu.cn, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <200805151137.10113.tjark.weber@gmx.de>*References*: <fb1efd203a02.3a02fb1efd20@whu.edu.cn> <200805151137.10113.tjark.weber@gmx.de>*User-agent*: Icedove 1.5.0.14pre (X11/20071025)

Trivially, analz(knows Spy []) is empty (see definitions). Tjark Weber wrote:

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 animplication "-->" in this subgoal. Because this premise is false, theimplication is trivially true.Best, Tjark

**References**:**[isabelle] about th proof of protocol***From:*jwang whu.edu.cn (jwang)

**Re: [isabelle] about th proof of protocol***From:*Tjark Weber

- Previous by Date: Re: [isabelle] about th proof of protocol
- Next by Date: Re: [isabelle] about th proof of protocol
- Previous by Thread: Re: [isabelle] about th proof of protocol
- Next by Thread: Re: [isabelle] about th proof of protocol
- Cl-isabelle-users May 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list