Email Gateway (Aug 18 2022 at 12:18): Email Gateway (Aug 18 2022 at 12:18):From: shadi shiri <shad_shirin@yahoo.com>
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
Email Gateway (Aug 18 2022 at 12:18):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
Maybe a way to model this could be modifying these:
constdefs
(* Signature = Message + signed Digest *)
sign :: "[key, msg]=>msg"
"sign K X == {| X, Crypt K (Hash X) |} "
(* Signature Only = signed Digest Only *)
signOnly :: "[key, msg]=>msg"
"signOnly K X == Crypt K (Hash X)"
(* Signature for Certificates = Message + signed Message *)
signCert :: "[key, msg]=>msg"
"signCert K X == {|X, Crypt K X |}"
I would write it this way:
mac :: "[key, msg]=>msg"
"mac K X == {| Hash Pair(K,X) |} "
To me it seems enough, since you need to treat the MAC function as a
black box that takes in count the message and a key, and outputs a
hash like thing.
The only trick in proofs regarding constdefs it that you need to
explicitly unfold them to go trough.
Jean
Last updated: May 03 2024 at 08:18 UTC