Re: [isabelle] ?? :the inductive approach analyze the NS protocol



Actually I had the same problem to start understanding the method. But as Larry told, it is everything in the JCS paper (page 19). Other interesting reading is Giampaolo's thesis.

The basic idea is that you first get rid of the existential quantification applying the introduction rules (this is basic theorem proving strategy). This leaves you with two sub-goals.

The second you eliminate directly, because it is the empty trace. Just give the inductive definition to the empty trace and voilà. To the other sub-goal, as the name of the lemma proposes it is the possibility, so you should give then the path to reach this possible state.

The 6 sub-goals produced, are basically the path construction to reach the state in the lemma. The you just apply the possibility, it will lead you to the proof by Isabelle's reasoner.



Jean


Lawrence Paulson escreveu:
Papers describing the modelling method are here: <http://www.cl.cam.ac.uk/~lp15/papers/protocols.html>

See especially <http://www.cl.cam.ac.uk/~lp15/papers/Auth/jcs.pdf>. The proof you mention is of a "possibility property" and is discussed on page 19 of that paper.

Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623    Fax: +44(0)1223 334678



------------------------------------------------------------------------





On 20 Mar 2008, at 02:55, jwang whu.edu.cn (jwang) wrote:

   I have processed the (/Isabelle/src/HOL/Auth/)NS_Public_Bad file in
Isabelle,but I am puzzled by some result from Isabelle.For example,









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