Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)

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

On 11 Oct 2010, at 20:01, Denis Butin wrote:

> 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

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