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