[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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and