Archive by category 'Isabelle'
 
Isabelle Group on Facebook
September 13th, 2007 By recluze

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

Read All

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.

Read All
Protocol Nonce Question
August 28th, 2007 By recluze

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 –>...

Read All
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...

Read All

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...

Read All

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

Read All