[isabelle] Another question on Isabelle/HOL

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. 


Attachment: Final verification.thy
Description: Binary data

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