*To*: Denis Butin <denis.butin at gmail.com>*Subject*: Re: [isabelle] HOL/Auth : extension to parts/analz/synth*From*: Jean Martina <Jean.Martina at cl.cam.ac.uk>*Date*: Mon, 28 Mar 2011 18:57:04 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTinTQ7mGC5LmARMPU6MhGn1ccJvAZvQL0Shictt+@mail.gmail.com>*References*: <AANLkTinTQ7mGC5LmARMPU6MhGn1ccJvAZvQL0Shictt+@mail.gmail.com>*Sender*: "J.E. Martina" <jem74 at hermes.cam.ac.uk>

Hi Denis, Looks like your problem is the synth without explicitly saying that T in H. Have you tried to write a rule for synth that creates Crypt T (Blind K X) for any T in H? Even though you are assuming that Crypt will come out of the Crypt rule, this specific case will not be yielded with certainty to assert parts_synth. I had similar issued extending the Inductive Method for secret sharing. I think you need "Blind2 [intro]: "[|X \<in> synth H; Key(K) \<in> H; Key(T) \<in> H|] ==> Crypt T (Blind K X) \<in> synth H". I think this will make things easier for you. In fact, implementation of new cryptographic primitives support has been on the raise. It would be nice if someone could just absorb them all assembling and bring it to the standard Isabelle distribution. Jean On 28 Mar 2011, at 18:04, Denis Butin wrote: > Hi all, > > I want to model blind signatures using the security protocol framework > from HOL/Auth. > > In Message.thy, I added a component to the msg datatype (Blind key > msg), and made the following changes to the inductive sets parts, > analz and synth: > > In parts: > | Blinded: "Blind K X \<in> parts H ==> X \<in> parts H" > | Blinded2: "Crypt T (Blind K X) \<in> parts H ==> Crypt T X \<in> parts H" > > In analz: > | Unblind [dest]: "[|Blind K X \<in> analz H; Key(K) \<in> analz > H|] ==> X \<in> analz H" > | Unblind2 [dest]: "[|Crypt T (Blind K X) \<in> analz H; Key(K) \<in> > analz H|] ==> Crypt T X \<in> analz H" > > In synth: > | Blind [intro]: "[|X \<in> synth H; Key(K) \<in> H|] ==> Blind K X > \<in> synth H" > > The important rule is Unblind2, others are there for consistency. > > Now, using this, I can't prove parts_synth [simp]: "parts (synth H) = > parts H \<union> synth H", and I strongly suspect it doesn't hold. > This is problematic, because lemmas about the Spy's behaviour use > this. > > Investigating what is used in the proof, it turns out the problem > comes directly from the interplay between Blinded2 and synth. However, > removing Blinded2 breaks analz_subset_parts. > > I tried formulating Unblind2 as a synth rule, but I wasn't able to > prove it either, plus it will probably break lemmas related to Fake. > > I then tried "externalising" Unblind2 as an axiom. After giving it > some thought, it seems like a really bad idea. > > I've been stuck on this for a couple of days, and would be grateful > for any help or ideas. > > Regards, > Denis >

**References**:**[isabelle] HOL/Auth : extension to parts/analz/synth***From:*Denis Butin

- Previous by Date: [isabelle] HOL/Auth : extension to parts/analz/synth
- Next by Date: Re: [isabelle] Vector of bools
- Previous by Thread: [isabelle] HOL/Auth : extension to parts/analz/synth
- Next by Thread: [isabelle] Proving two real^3 spaces are the same
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list