Re: [isabelle] prooving protocols



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

On 19 Nov 2010, at 08:32, Lawrence Paulson wrote:

> 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
> 
> 
> On 18 Nov 2010, at 17:40, Novio wrote:
> 
>> 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
>> 
> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.