Security Engineering Research Group

Isabelle Group on Facebook

I have just joined Facebook. It looks like a much cleaner community than Orkut. I’ve found a new group about Isabelle there and have sent you guys an invitation. Join up if you feel like it. It can be a good resource for the future and for bringing together a nice group of researchers.
http://www.facebook.com/group.php?gid=18553699736

Security Engineering on Isabelle World Map

Now, the world can know that we’re working with Isabelle. Check out Isabelle’s world map here. And Tobias Nipkow was here in Peshawar! In March. When I was working my head off trying to get to grips with Isabelle. That was a chance missed.

Protocol Nonce Question

I have a question and I was wondering if one of you security gurus can answer it.

There’s a lemma in the “Message” theory in Isabelle. It says, “In any message, there is an upper bound N on its greatest Nonce”.

In Isabelle:

lemma “Ex N. !!n. N <=n –> Nonce n ~: parts {msg}”

The lemma, translated to English says, “There exists an N such that for all Nonces, if N is less than the nonce, this greater Nonce is not in the message” or “there is a Nonce of number n which is not in the message”.

Can somebody shed some light on why this might be so? Or why we’re bothering with proving this?

Note: Isabelle protocol verification theory does not give any motivation for the lemmas it’s proving. It’s just going about merrily proving all sort of seemingly repetitive theorems.

Protocol Verification in Isabelle

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.

Specification/Verification in Isabelle Finally Starting

Alright. After much waiting and detours, I’ve finally decided to start doing some original work in Isabelle/HOL itself. *drum rolls*

After the last meeting with Mr. MM, I’ve decided to start working on the specification I’ve already done in Z of his framework. The specification is pretty involved and would require much more work to be properly embedded in HOL. I have a few ideas but that will have to wait.

Mr. MM: Here’s my plan. First of all, what needs to be done is that we need to have the Document Model formalized, specified and verified. This has already been done during HOL-OCL development by the ETH Zurich guys but I would like to do it in a more accessible way (i.e. without the use of stuff like “smashed sets and objects”). I want to make something that can be used by the average formal specification engineer. If we can get only this done, it would be an accomplishment.

So, I would appreciate it if you can take some time out and find out for me if the Class Diagrams of UML have been formalized in Isabelle/HOL. I’ve done thorough searching and have only found stuff done in either HOL-Z or HOL-OCL (all by the ETH guys). I want to make sure that I’m not re-inventing the wheel. I’ll continue my search but it would be a big help if you can confirm that it has not been done before or find me the papers which have done it.

HOL-OCL Installation Instructions Posted

Instructions posted on:

http://recluze.wordpress.com/2007/06/17/installing-and-configuring-hol-ocl/