Email Gateway (Aug 18 2022 at 16:29): Email Gateway (Aug 18 2022 at 16:29):From: Novio <novio@azet.sk>
Hi,
I didnt find any material about how to
proove something in Isabelle. I need
to proove security protocols. I found
that in installation package in Isabelle
are some protocols but I didnt find in
Isabelle's web page what to do exactly,
which button to push to begin prooving.
Thanks, PH
Email Gateway (Aug 18 2022 at 16:29):From: Lawrence Paulson <lp15@cam.ac.uk>
You will find ample documentation on our website:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html
Isabelle is not a push-button verifier. It takes some time to learn, and security protocol verification is one of the more demanding applications. Push-button security protocol verifiers do exist, and possibly you should obtain one of those.
Larry Paulson
Email Gateway (Aug 18 2022 at 16:30):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
Complementing Larry's comments: You can start by looking to other automatic methods such as Graham Steel's and Christopher Weidenbach's approaches. They are a good way to understand how protocol verification works under an inductive framework, but with automation. This can clearly cut some corners when you got to do protocol verification with Isabelle. If you are really interested in Higher-Order formalisation for that, you can start by reading Larry's JCS paper on the Inductive Method and/or Giampaolo Bella's book on Formal Correctness of Security Protocols.
Jean
Last updated: Apr 24 2024 at 20:16 UTC