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.

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…

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.

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.

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.

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.

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.

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.

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