Email Gateway (Aug 18 2022 at 17:26): Email Gateway (Aug 18 2022 at 17:26):From: Denis Butin <denis.butin@gmail.com>
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
Email Gateway (Aug 18 2022 at 17:27):From: Jean Martina <Jean.Martina@cl.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
Last updated: Nov 21 2024 at 12:39 UTC