Re: [isabelle] The last question- on isabelle/HOL



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


On 18 Aug 2008, at 15:07, shadi shiri wrote:

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.







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