[isabelle] I have a question on isabelle/HOL
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 protoclo,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 e with your valuable information.
This archive was generated by a fusion of
Pipermail (Mailman edition) and