Email Gateway (Aug 18 2022 at 12:18): Email Gateway (Aug 18 2022 at 12:18):From: shadi shiri <shad_shirin@yahoo.com>
Dear Sir or Madam,
I tried to analyz kryptoknight protocol by isabelle tool. It is like otway-Rees.
According my previous questions I model MAC function by Crypt(key) Hash X.
Of course it can not be cryptographicaly true,but it works for the verification.
Because of the similarity I used most of the theorem in otway-Rees verification.
Enclosed the mail,is the ".thy" file of my job. It will be truely kind of you to have a look,
and tell me your idea. I also have a problem. Although the tool can pass all the steps for verifying lemmas,
it shows an error when it reaches the "done" step,and displays:"failed to finish proof after successful terminal methods" .It happens even for very simple lemmas.
Would you please tell me what is the reason.
Thank you very much
Shadi Shiri
P.S: I know that this e-mail address is for problems with the tools, but it would be very kind of you,as professionals, to answer my questions and suggest me about how to verify this protocol better by better lemmas.
Final verification.thy
Last updated: May 03 2024 at 08:18 UTC