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




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

From: shadi shiri <shad_shirin at yahoo.com>
Subject: Re: [isabelle] I have a question on isabelle/HOL
To: "Lawrence Paulson" <lp15 at cam.ac.uk>
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 cam.ac.uk> wrote:

From: Lawrence Paulson <lp15 at cam.ac.uk>
Subject: Re: [isabelle] I have a question on isabelle/HOL
To: shad_shirin at yahoo.com
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:

http://www.cl.cam.ac.uk/~lp15/papers/protocols.html

Larry

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.