[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:
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 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.
Sincerely yours
Shadi Shiri

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