Re: [isabelle] HOL/Auth subgoal (Nonce secrecy)
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))
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and