Re: [isabelle] Fw: Re: I have a question on isabelle/HOL

	Maybe a way to model this could be modifying these:

(* 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.


On 16 Aug 2008, at 17:18, shadi shiri wrote:

--- On Fri, 8/15/08, shadi shiri <shad_shirin at> wrote:

From: shadi shiri <shad_shirin at>
Subject: Re: [isabelle] I have a question on isabelle/HOL
To: "Lawrence Paulson" <lp15 at>
Date: Friday, August 15, 2008, 10:11 PM

Dear Mr.Palson
I am very happy to be in touch with a great man in computer science.
According to your answer,I searched isabelle libraries, but it didn't help. would you please be a little more specific and tell me how I can write a step of this protocol,containing MAC function. Since I tried Hash[shrK a] x, Hash [shrK A,X] and other forms,and they all make some errors,I need a specific example.
Please again do me a favor and help me with your valuable information.
Thank you
Shadi Shiri
--- On Fri, 8/15/08, Lawrence Paulson <lp15 at> wrote:

From: Lawrence Paulson <lp15 at>
Subject: Re: [isabelle] I have a question on isabelle/HOL
To: shad_shirin at
Date: Friday, August 15, 2008, 1:43 PM

To create a message authentication code, you need a secret shared with
the opposite party. Then, you form the cryptographic hash of your
message with this secret. The Isabelle theories support cryptographic
hashing, so this protocol should be easy to model. For background
information on the method, I suggest that you read one or more of the
introductory papers listed at the following page:


On 14 Aug 2008, at 20:14, shadi shiri wrote:

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

Larry Paulson

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