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