[isabelle] HOL/Auth : extension to parts/analz/synth
I want to model blind signatures using the security protocol framework
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:
| 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"
| 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"
| 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and