*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] about th proof of protocol*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Thu, 15 May 2008 11:37:10 +0200*Cc*: jwang at whu.edu.cn*In-reply-to*: <fb1efd203a02.3a02fb1efd20@whu.edu.cn>*References*: <fb1efd203a02.3a02fb1efd20@whu.edu.cn>*User-agent*: KMail/1.8

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

**Follow-Ups**:**Re: [isabelle] about th proof of protocol***From:*Cristiano Longo

**Re: [isabelle] about th proof of protocol***From:*Jean Martina

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

- Previous by Date: [isabelle] Research Position in Computer Science at The Australian National University
- Next by Date: Re: [isabelle] about th proof of protocol
- Previous by Thread: [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