# [isabelle] 转发 :the inductive approach analyze the NS protocol

--- Begin Message ---
```   hello,everyone:

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,

when the lemma: "\<exists>NB. \<exists>evs \<in>ns_public. Says A B
(Crypt (pubEK B) (Nonce NB)) \<in> set evs"  was processed in
NS_Public_Bad file, the following six subgoal was given .

I don't understand why the six subgoals was produced and how the
inductive approach analyze the lemma?
the six subgoals is shown  as follows:
proof (prove): step 2
goal (6 subgoals):
1. Says A B (Crypt (pubK B) (Nonce ?NB))
: set [Says ?A2 ?B2 (Crypt (pubK ?B2) (Nonce ?NB2)),
Says ?B3 ?A3 (Crypt (pubK ?A3) {|Nonce ?NA3, Nonce ?NB3|}),
Says ?A4 ?B4 (Crypt (pubK ?B4) {|Nonce ?NA4, Agent ?A4|})]
2. Nonce ?NA4 ~: used []
3. Nonce ?NB3
~: used [Says ?A4 ?B4 (Crypt (pubK ?B4) {|Nonce ?NA4, Agent ?A4|})]
4. Says ?A'3 ?B3 (Crypt (pubK ?B3) {|Nonce ?NA3, Agent ?A3|})
: set [Says ?A4 ?B4 (Crypt (pubK ?B4) {|Nonce ?NA4, Agent ?A4|})]
5. Says ?A2 ?B2 (Crypt (pubK ?B2) {|Nonce ?NA2, Agent ?A2|})
: set [Says ?B3 ?A3 (Crypt (pubK ?A3) {|Nonce ?NA3, Nonce ?NB3|}),
Says ?A4 ?B4 (Crypt (pubK ?B4) {|Nonce ?NA4, Agent ?A4|})]
6. Says ?B'2 ?A2 (Crypt (pubK ?A2) {|Nonce ?NA2, Nonce ?NB2|})
: set [Says ?B3 ?A3 (Crypt (pubK ?A3) {|Nonce ?NA3, Nonce ?NB3|}),
Says ?A4 ?B4 (Crypt (pubK ?B4) {|Nonce ?NA4, Agent ?A4|})]

Jean

sincerely

```

--- End Message ---

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