[isabelle] HOL/Auth subgoal (Nonce secrecy)



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.