Email Gateway (Aug 18 2022 at 11:11): Email Gateway (Aug 18 2022 at 11:11):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
Hello,
I'm studing the inductive Approach to verifying cryptograpgic protocols.I have consulted the protocol proof therory from the address(http://isabelle.in.tum.de/library/HOL/Auth/index.html ), but I found some detailed proof procedure were not described in the theory file.I need the detailed proof theory of NS_Public_Bad protocol or other protocol. Anyone can help me?
regards,
Jane
Email Gateway (Aug 18 2022 at 11:12):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
Firstly, Thanks a lot for your reply message ,but it can't help me.I think inductive approach to verifying cryptograpgic protocols need induction over traces.For NS_Public_Bad protocol,every theroy need induction over five traces(Nil,Fake,NS1,NS2,NS3) of protocol model and yields five subgoals by induction,but the induction procedure was not described in NS_Publi c_Bad.thy ,only the proof commands. So I don't understand how some theorems were reasoned by induction.I wish to get more detailed documents about protocol goal induction,that will help me understand your inductive approach to verifying cryptograpgic protocols. Wish to get the documents including detailed inductive steps of NS_Public_Bad protocol.
Sincerely
Jane
----- 原邮件 -----
从: Lawrence Paulson <lp15@cam.ac.uk>
日期: 星期一, 一月 7日, 2008 下午8:25
主题: Re: [isabelle] About the Inductive Approach to verifying cryptograpgic protocols
To: "jwang whu.edu.cn" <jwang@whu.edu.cn> (jwang)
Cc: cl-isabelle-users@lists.cam.ac.uk
Email Gateway (Aug 18 2022 at 11:12):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: RIPEMD160
Probably you are trying to do the same I tried some time ago. Doing by
hand the proofs Isabelle constructs. It is not impossible, but hard to
accomplish, since that when you are starting to prove some protocol, you
import a base theory (in this case: imports Public begin), that will
import its own base theories, and so on. Some of these theories also
have restrictions on how to proceed the proofs, that you will need
always to remember.
All this will make the proofs even harder to accomplish than by using
Isabelle. For example it is a nightmare to prove by hand anything that
relates with the use of Public keys. I can tell you its not worth. Just
trust Isabelle :p
About your problem you cited, after revising the (src/HOL/Auth/)
NS_Public_Bad.thy , it is there the inductive definition:
inductive ns_public
intros
(Initial trace is empty)
Nil: "[] ? ns_public"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake: "?evsf ? ns_public; X ? synth (analz (spies evsf))?
? Says Spy B X # evsf ? ns_public"
(Alice initiates a protocol run, sending a nonce to Bob)
NS1: "?evs1 ? ns_public; Nonce NA ? used evs1?
? Says A B (Crypt (pubEK B) ?Nonce NA, Agent A?)
# evs1 ? ns_public"
(Bob responds to Alice's message with a further nonce)
NS2: "?evs2 ? ns_public; Nonce NB ? used evs2;
Says A' B (Crypt (pubEK B) ?Nonce NA, Agent A?) ? set evs2?
? Says B A (Crypt (pubEK A) ?Nonce NA, Nonce NB?)
# evs2 ? ns_public"
(Alice proves her existence by sending NB back to Bob.)
NS3: "?evs3 ? ns_public;
Says A B (Crypt (pubEK B) ?Nonce NA, Agent A?) ? set evs3;
Says B' A (Crypt (pubEK A) ?Nonce NA, Nonce NB?) ? set evs3?
? Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 ? ns_public"
When you have commands such as:
lemma "?NB. ?evs ? ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) ?
set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN
ns_public.NS2,THEN ns_public.NS3])
by possibility
you are directly reasoning over the inductive definition above. Can you
explain better what you are trying to do? Maybe we can exchange some
experience, since I am working exactly in extending this.
Regards,
Jean
jwang whu.edu.cn (jwang) wrote:
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2 (GNU/Linux)
Comment: Using GnuPG with SUSE - http://enigmail.mozdev.org
iD8DBQFHhKOZQN0Max56WicRAxhFAJ4kAw9uprwzPGVpBI2dZX0baX+5PgCgmsS4
qCTcJZ9ZBNnpml5yGAIEAmg=
=lHJf
-----END PGP SIGNATURE-----
Last updated: May 03 2024 at 01:09 UTC