Email Gateway (Aug 18 2022 at 11:13): Email Gateway (Aug 18 2022 at 11:13):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
cryptograpgic protocols
X-Accept-Language: zh-CN
Priority: normal
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: 7bit
Thanks for your help!
Now, I' m studing the inductive approach to verifying cryptograpgic
protocols.Indeed I try to do the proofs Isabelle constructs by hand,but
now maybe I should give up it.I wish to understand more clearly the
inductive approach by the detailed documents about protocol goal
induction and reasoning procedure ,so that I could apply inductive
approach to verifying some other protocols.
sincerely
Jean
Email Gateway (Aug 18 2022 at 11:13):From: Lawrence Paulson <lp15@cam.ac.uk>
These proofs cannot easily be done by hand. I am told that people
tried to mechanise these proofs using a Certain Other Well-Known
Prover, but gave up.
A form of hard proof that most closely resembles the inductive
approach is the "strand spaces" method <http://www.mitre.org/tech/strands/
.
Use the references I sent in an earlier email for more background
information.
Larry Paulson
Email Gateway (Aug 18 2022 at 11:14):From: Gergely Buday <gbuday@gmail.com>
jwang wrote:
Learning Isabelle is not easy on your own and if you take the burden
of learning the inductive method at the same time, well, you do not
make your life easy. I recommend you to execute the proof scripts
step-by-step, and see what the proof commands do. Following an
Isabelle proof step-by-step is the start to create your own proofs,
but there is a long way to it.
Reading the Isabelle/HOL tutorial and doing the exercises of it should
help, but I guess you have already looked inside.
Last updated: May 03 2024 at 04:19 UTC