Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 转发 :the inductive approach analyze the NS pr...

Email Gateway (Aug 18 2022 at 11:35):

From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
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

Email Gateway (Aug 18 2022 at 11:35):

From: Lawrence Paulson <lp15@cam.ac.uk>
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
Lawrence Paulson.vcf

Last updated: May 03 2024 at 12:27 UTC