Email Gateway (Aug 18 2022 at 16:12): Email Gateway (Aug 18 2022 at 16:12):From: Denis Butin <denis.butin@gmail.com>
Hi all,
I am using the security protocol framework from HOL/Auth, and I am
frustratingly stuck on the following subgoal:
[A \<notin> bad; R \<notin> bad;
evsp1 \<in> ns_public_pki;
Says A B (Crypt (pubK R) {Nonce NC, Agent A}) \<in> set evsp1;
Nonce NC \<notin> analz (knows Spy evsp1);
Nonce NC \<in> analz (insert (Key (pubK Aa)) (insert {Agent
Aa, Number certa} (knows Spy evsp1)))]
==> False
It seems easy: I just have to show that adding a public key, an
agent's name and a number to the Spy's knowledge doesn't change the
secrecy of the nonce NC, which leads to the required contradiction.
The following lemmas seem helpful:
privateKey_neq_publicKey (a private key can never be a public key,
hence pubK Aa cannot be the inverse of pubK R) ;
parts_insert_spies ( parts (insert ?X (knows Spy ?evs)) = parts {?X}
\<union> parts (knows Spy ?evs));
analz_into_parts, which is already declared as [dest] at the
beginning of my theory;
knows_Cons, which is part of the inductive definition of the knows function.
My only problem is how to put them together; I unsuccessfuly tried things like
apply (auto intro: privateKey_neq_publicKey knows_Cons simp add:
parts_insert_spies)
I am not too sure on the best way to use/combine auto or blast with
existing lemmas, so I may have missed something obvious.
Sledgehammer suggested a metis command which resulted in an Ill-typed
instantiation error.
Many thanks for reading this, and for any help.
Regards,
Denis
Email Gateway (Aug 18 2022 at 16:12):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Denis,
Sledgehammer suggested a metis command which resulted in an Ill-typed
instantiation error.
I'll let others answer the rest of your email, but when this happens one solution is to try passing the "full_types" option to Sledgehammer:
sledgehammer [full_types]
(See the manual sledgehammer.pdf for details.) Then the encoding used is somewhat heavier but is much less likely to cause metis failures.
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 16:12):From: Lawrence Paulson <lp15@cam.ac.uk>
Any theorem involving the function analz requires special care. As you say, this one is conceptually trivial because all the information being added to the spy's knowledge is already publicly available. But you still have to go about the proof in the right way.
This subgoal appears to be unsimplified. The standard setup of simplification rules for analz is designed to deal with this sort of term. They permute the inserted items so that trivial ones (such as agent names) are called to the front and then taken outside of the analz call altogether. So try
apply (simp add: analz_insert_eq pushes split_ifs)
You should be left with nothing but the key. For a secrecy theorem, dealing with the key is complicated, and you need to use some of the measures outlined in section 4.5 of my paper “The Inductive Approach to Verifying Cryptographic Protocols”. But because this is a public key, you should only need to use the theorem Set.insert_absorb to erase it. In fact you probably won't need this final step, because analz_insert_eq above should take care of it. Good luck!
Larry Paulson
Email Gateway (Aug 18 2022 at 16:12):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
Larry/Denis
I think the problem here has to do with the proof strategy you are taking. It is not unusual you ending up with these complications (double insert inside an analz) if you are too aggressive at the beginning of the proof. Larry's reading recommendation can be complemented by chapter 4 in Giampaolo Bella's book.
If you want to post privately the entire lemma and the proof commands you written so far I can take a look to see if it is one of the usuals.
Regards,
Jean
Email Gateway (Aug 18 2022 at 16:13):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Jean,
(I'm taking the liberty of answering to the mailing list.)
From my own trial and error experiences in this specific domain inside Isabelle, E and vampire tend to give a lot of ill-typed translations.
SPASS on the other hand don't do that often. A critical issue in his initial problem is the willing to inspect the analz set. I would say (empirically again) that 80% of sledgehammer's output in this situation is ill-typed.
That's a lot (Nipkow & Boehme found it was < 10% on their test data), but it's known to vary from theory to theory. SPASS is usually run with the SOS (set of support) strategy, which might make it less likely that it finds (untyped) contradictions between the included facts.
If you enable fuil_types, you need around 5 times more CPU time to arrive to the same results (again just considering this domain, I did the test 2 years ago), so in the end it is worth to get some ill-typed results that you can sieve out quickly.
And have you tried playing with the "no_atp" (previously "noatp") attribute? Unsound proofs tend to always involve the same facts, and using this tag you can instruct Sledgehammer to leave them out. Alternatively, with 2009-2, you can try the syntax
sledgehammer (del: evil_facts_go_here)
We haven't given up all hopes of coming up with a sound (or at least sounder) yet efficient encoding for Sledgehammer, but in the meantime these are the workarounds.
Regards,
Jasmin
Email Gateway (Aug 18 2022 at 16:13):From: Jean Martina <Jean.Martina@cl.cam.ac.uk>
This number i cited above is a specific case where sledgehammer need to deal with the analz function. Probably it does not have anything to do with Sledgehammer, but with the way things are thrown to it. I noticed that the rate of success of sledgehammer is dependent on the way you generate and prepare the subgoals to be sledgehammered.
Jean
Email Gateway (Aug 18 2022 at 16:13):From: Denis Butin <denis.butin@gmail.com>
Hi all,
Thank you for those helpful answers.
Simon: I saw your presentation at FLOC and found the framework very
interesting; however, for my protocol I had to modify Public.thy and
Event.thy, so this might be a problem. What do you think?
Jasmin: I tried sledgehammer [full_types], but unfortunately it timed
out even with a limit of 10 minutes.
Larry: Thanks, this is helpful. I was able to conclude the proof with
pushes and insert_absorb. The only problem that remains is that to do
this, I had to allow the Spy to have initial knowledge of all public
keys, which I didn't assume initially for this particular setting.
Ideally, I would like to find a way to go from
Nonce NC \<in> analz (insert (Key (pubK Aa)) (knows Spy evsp1))
to
Nonce NC \<in> analz (insert (knows Spy evsp1))
that would only use the fact that a pubK can never decode a ciphertext
encrypted with another pubK. privateKey_neq_publicKey seems a nice
candidate for this, but I seem to need something additional.
Jean: I'll send you an email then.
Kind regards,
Denis
Email Gateway (Aug 18 2022 at 16:13):From: Lawrence Paulson <lp15@cam.ac.uk>
If it is plausible that the spy could possess this particular public key, then it's unrealistic to assume he doesn't. So it makes sense to assume that he possesses all public keys. And it will make the proof very much simpler. To do what you want for a key that isn't known to the spy requires a full-blown confidentiality proof, which is a big deal.
Larry Paulson
Email Gateway (Aug 18 2022 at 16:13):From: Simon Meier <iridcode@gmail.com>
Hi Denis,
Simon: I saw your presentation at FLOC and found the framework very
interesting; however, for my protocol I had to modify Public.thy and
Event.thy, so this might be a problem. What do you think?
Hmm, it depends on the changes. The question is, if you can model your
protocol as a set of linear roles and if you can evaluate your security
property over the state our security protocol model provides. If yes, then
our framework might be of quite some help to you. Otherwise, your problem
might be amenable (in the future) to the generalization of the protocol
model that I am working on.
In any case, I would be very interested in seeing the protocol you are
investigating in order to guide me where the put my resources. For example
in the form of your source files. If you'd have an informal description of
the protocol, then this would probably help me understand your sources.
best regards,
Simon
Last updated: May 07 2024 at 01:07 UTC