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



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





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