Email Gateway (Aug 18 2022 at 11:53): Email Gateway (Aug 18 2022 at 11:53):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
hello,
I 'm studing the proof procedure of Ns_Public_Bad protocol in Isabelle.How some theorem are proved in NIL([] trace) puzzled me greatly.For example ,theorem Spy_not see_NA.When applying "erule ns_public.induct", five subgoals will be given.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.
& nbsp; &n bsp; Jean
Email Gateway (Aug 18 2022 at 11:53):From: Tjark Weber <tjark.weber@gmx.de>
Jean,
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
Email Gateway (Aug 18 2022 at 11:53):From: Cristiano Longo <cristiano.longo@tvblob.com>
Trivially, analz(knows Spy []) is empty (see definitions).
Tjark Weber wrote:
Email Gateway (Aug 18 2022 at 11:54):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
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:
Last updated: May 03 2024 at 04:19 UTC