Email Gateway (Aug 18 2022 at 12:19): Email Gateway (Aug 18 2022 at 12:19):From: shadi shiri <shad_shirin@yahoo.com>
Dear professionals,
Than you for the kind consideration. It encourages me to try more. I corrected my model by the help of
your answer. It gets realy like Otway-Rees.
But it is still too slow and can not prove the lemmas. It would be realy kind of you if you do me your last favor and tell me what is the reason and how I can fix it.
I have enclosed the file by this e-mail.
Thank you very much
Regards
Shadi Shiri
Final Kryptonight.thy
Email Gateway (Aug 18 2022 at 12:19):From: Lawrence Paulson <lp15@cam.ac.uk>
I took a look at your file. The problem is that these properties
typically require inductive proofs, but you simply invoke "blast" and
expect Isabelle to do the rest. Secrecy properties are difficult to
prove and they are not suitable as exercises for beginners. I suggest
that you read the Isabelle tutorial and spend some months working on
simpler problems before attempting to verify security protocols.
Larry Paulson
Last updated: May 03 2024 at 12:27 UTC