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

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
On 12 Oct 2010, at 17:39, Denis Butin wrote:
> 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.

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