Re: [isabelle] HOL/Auth : extension to parts/analz/synth



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
> 






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