Protocol Verification in Isabelle
August 22nd, 2007 By recluze

I’ve started working with the development of framework for protocol verification part of my Isabelle related work. Currently, this is simply copying of the Messages, Events and Public-key portion provided with Isabelle. This is mostly for my understanding. It’s already developed and many helpful theorems are already proven. They can be used as-is but that would mean a lot of efforts during our own proofs.

I’ll be posting my progress (in the form of regularly created PDF) here as it’s already publicly available on the internet: It’s mostly to show anyone interested what my progress/status is.

Download the PDF here.

8 Responses to " Protocol Verification in Isabelle "
 
TaMLeEk
August 24th, 2007

Thats good to have pdf’s about the varification related work.. one concern that i feel is that how ll we manage the namings of the lemma’s and theories etc… As we ll be embedding many theories in our high level security protocols varifications…

 
recluze
August 25th, 2007

I don’t really understand what you mean by “embedding many theories”. Isabelle uses the standard syntax of TheoryName.LemmaName syntax. So, there’s no problem of clashes.

 
shazkhan
August 25th, 2007

We’ll knowing nothing about formal verification all I can say is that you have to make a logical sense out of all the protocols that work together for your task. That would require a comon naming scheme which would fit in all the variables and constants of the protocols. In simple words make a meta protocol with w.r.t. to the theories.

 
recluze
August 26th, 2007

I agree shaz but this stuff is done automatically in Isabelle. The workflow of Isabelle ensures that you do it properly. The theories work like modules and the lemmas and theorems are automatically kept separated. So, no problem with that.

About the meta-protocol approach, that’s what we mean when we formalize public key architecture without the specification of its usage.

 
recluze
August 27th, 2007

Update: I’ve worked some more on the message formalization. The unions of messages are now done.

I think it would be easy to just post updates as comments to this post instead of creating new posts each time I upload a revised version. The above PDF will always point to the latest uploaded file. So, if you want to follow the progress, bookmark this post.

I will be glad to answer any questions you may have regarding these lemmas. They seem disconnected right now but I think I know where they’re going. Your questions will help me too. So, don’t hesitate.

 
recluze
August 29th, 2007

Update: Some more work. I’m finished with “parts” of a message. I’ve also started work on “analz” — information that can be extracted from a message.

One achievement in all this: take a look at lemma “parts_analz”. My proof for this lemma is certainly easier to comprehend than the one given in the “official” theory file. I don’t know whether it’s more efficient but since it’s proved within a split second, the procedure really doesn’t matter.

Of course, if there’s some problem with this way, I’d like to know.

 
recluze
September 7th, 2007

Update: more work done. Now, I’m on to proving idempotence properties of analz.

I’m getting more and more comfortable with the actual lemma proving. I can now prove many lemmas without looking at the proofs in the theory.

This is getting more and more interesting.

 
recluze
September 7th, 2007

Note:

If you’ve used Isabelle and you’ve come across iprover, here’s what it means:

——————
The second question that I want to ask here is maybe very naive, but I do not feel shame. Is it possible to use isabelle just to check it a propositional formula is intuionistically valid, or just classically valid? For example: can isabelle tell me that (p \lor \neg p) is not (intuitionistically) valid? And what about first order intuitionist

apply iprover (* for intuitionistic logic *)
apply blast (* for classical logic *)

Regards
Tobias
——————

Source

Leave a Reply


(Required)

(Required)