# [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.*