[isabelle] I have a question on isabelle/HOL

--- On Thu, 8/14/08, shadi shiri <shad_shirin at yahoo.com> wrote:

From: shadi shiri <shad_shirin at yahoo.com>
Subject: I have a question on isabelle/HOL
To: isabelle-users at cl.cam.ac.uk
Date: Thursday, August 14, 2008, 11:44 PM

Dear Sir or Madam,
I am an IT engineer interested in formal verification of protocols.Recently I have installed Isabelle theorem prover.
For the first try I wanna prove the Kryptoknight protocol features. the protocol is like this:
A-->B:       Na
B-->KDC: Na,Nb,A
KDC-->B: Mac a(Na,Kab,B),Ea [Mac a(Na,Kab,B)]+ Kab, 
               Mac b(Na,Kab,A),Eb [Mac b(Na,Kab,A)]+ Kab
B-->A:     Mac ab(Na,Nb,B),Mac a(Na,Kab,B),Ea [Mac a(Na,Kab,B)]+ Kab
A-->B:     Mac ab(Na,Nb)
As you see it looks some how like the otway-Rees protocol,But it uses Mac functions. I want to know how I can model these
functions in isabelle. And I am also interested in knowing if this protocol has ever been verified by a professional and how,
Since I tried and as a result of being unexperienced I couldn't be successful in this job.
Please help me with your valuable information.
Sincerely yours
Shadi Shiri

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