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.
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