Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: desktop_app.scala Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Auth/NS_Public_Bad.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
Flawed version, vulnerable to Lowe's attack.

From page 260 of
  Burrows, Abadi and Needham.  A Logic of Authentication.
  Proc. Royal Soc. 426 (1989)
*)

section\<open>Verifying the Needham-Schroeder Public-Key Protocol\<close>

theory NS_Public_Bad imports Public begin

inductive_set ns_public :: "event list set"
  where
         (*Initial trace is empty*)
   Nil:  "[] \ ns_public"

         (*The spy MAY say anything he CAN say.  We do not expect him to
           invent new nonces here, but he can also use NS1.  Common to
           all similar protocols.*)
| Fake: "\evsf \ ns_public; X \ synth (analz (spies evsf))\
          \<Longrightarrow> Says Spy B X  # evsf \<in> ns_public"

         (*Alice initiates a protocol run, sending a nonce to Bob*)
| NS1:  "\evs1 \ ns_public; Nonce NA \ used evs1\
          \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
                # evs1  \<in>  ns_public"

         (*Bob responds to Alice's message with a further nonce*)
| NS2:  "\evs2 \ ns_public; Nonce NB \ used evs2;
           Says A' B (Crypt (pubEK B) \Nonce NA, Agent A\) \ set evs2\
          \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
                # evs2  \<in>  ns_public"

         (*Alice proves her existence by sending NB back to Bob.*)
| NS3:  "\evs3 \ ns_public;
           Says A  B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
           Says B' A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs3\
          \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public"

declare knows_Spy_partsEs [elim]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]

(*A "possibility property": there are traces that reach the end*)
lemma "\NB. \evs \ ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \ set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2,
                                   THEN ns_public.NS3])
by possibility

(**** Inductive proofs about ns_public ****)

(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
    sends messages containing X! **)

(*Spy never sees another agent's private key! (unless it's bad at start)*)
lemma Spy_see_priEK [simp]:
      "evs \ ns_public \ (Key (priEK A) \ parts (spies evs)) = (A \ bad)"
by (erule ns_public.induct, auto)

lemma Spy_analz_priEK [simp]:
      "evs \ ns_public \ (Key (priEK A) \ analz (spies evs)) = (A \ bad)"
by auto

(*** Authenticity properties obtained from NS2 ***)

(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
  is secret.  (Honest users generate fresh nonces.)*)
lemma no_nonce_NS1_NS2 [rule_format]:
      "evs \ ns_public
       \<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
           Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
           Nonce NA \<in> analz (spies evs)"
apply (erule ns_public.induct, simp_all)
apply (blast intro: analz_insertI)+
done

(*Unicity for NS1: nonce NA identifies agents A and B*)
lemma unique_NA:
     "\Crypt(pubEK B) \Nonce NA, Agent A \ \ parts(spies evs);
       Crypt(pubEK B') \Nonce NA, Agent A'\ \ parts(spies evs);
       Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
      \<Longrightarrow> A=A' \<and> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule ns_public.induct, simp_all)
(*Fake, NS1*)
apply (blast intro!: analz_insertI)+
done

(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure
  The major premise "Says A B ..." makes it a dest-rule, so we use
  (erule rev_mp) rather than rule_format. *)
theorem Spy_not_see_NA:
      "\Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs;
        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
       \<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
apply (erule rev_mp)
apply (erule ns_public.induct, simp_all, spy_analz)
apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
done

(*Authentication for A: if she receives message 2 and has used NA
  to start a run, then B has sent message 2.*)
lemma A_trusts_NS2_lemma [rule_format]:
   "\A \ bad; B \ bad; evs \ ns_public\
    \<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
        Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
        Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
apply (erule ns_public.induct)
apply (auto dest: Spy_not_see_NA unique_NA)
done

theorem A_trusts_NS2:
     "\Says A B (Crypt(pubEK B) \Nonce NA, Agent A\) \ set evs;
       Says B' A (Crypt(pubEK A) \Nonce NA, Nonce NB\) \ set evs;
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
      \<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
by (blast intro: A_trusts_NS2_lemma)

(*If the encrypted message appears then it originated with Alice in NS1*)
lemma B_trusts_NS1 [rule_format]:
     "evs \ ns_public
      \<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
          Nonce NA \<notin> analz (spies evs) \<longrightarrow>
          Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
apply (erule ns_public.induct, simp_all)
(*Fake*)
apply (blast intro!: analz_insertI)
done

(*** Authenticity properties obtained from NS2 ***)

(*Unicity for NS2: nonce NB identifies nonce NA and agent A
  [proof closely follows that for unique_NA] *)
lemma unique_NB [dest]:
     "\Crypt(pubEK A) \Nonce NA, Nonce NB\ \ parts(spies evs);
       Crypt(pubEK A') \Nonce NA', Nonce NB\ \ parts(spies evs);
       Nonce NB \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
     \<Longrightarrow> A=A' \<and> NA=NA'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule ns_public.induct, simp_all)
(*Fake, NS2*)
apply (blast intro!: analz_insertI)+
done

(*NB remains secret PROVIDED Alice never responds with round 3*)
theorem Spy_not_see_NB [dest]:
     "\Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs;
       \<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs;
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
     \<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule ns_public.induct, simp_all, spy_analz)
apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
apply (blast intro: no_nonce_NS1_NS2)+
done

(*Authentication for B: if he receives message 3 and has used NB
  in message 2, then A has sent message 3--to somebody....*)

lemma B_trusts_NS3_lemma [rule_format]:
     "\A \ bad; B \ bad; evs \ ns_public\
      \<Longrightarrow> Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
          Says B A  (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
          (\<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs)"
apply (erule ns_public.induct, auto)
by (blast intro: no_nonce_NS1_NS2)+

theorem B_trusts_NS3:
     "\Says B A (Crypt (pubEK A) \Nonce NA, Nonce NB\) \ set evs;
       Says A' B (Crypt (pubEK B) (Nonce NB)) \ set evs;
       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_public\<rbrakk>
      \<Longrightarrow> \<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs"
by (blast intro: B_trusts_NS3_lemma)

(*Can we strengthen the secrecy theorem Spy_not_see_NB?  NO*)
lemma "\A \ bad; B \ bad; evs \ ns_public\
       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs
           \<longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule ns_public.induct, simp_all, spy_analz)
(*NS1: by freshness*)
apply blast
(*NS2: by freshness and unicity of NB*)
apply (blast intro: no_nonce_NS1_NS2)
(*NS3: unicity of NB identifies A and NA, but not B*)
apply clarify
apply (frule_tac A' = A in
       Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
apply (rename_tac evs3 B' C)
txt\<open>This is the attack!
@{subgoals[display,indent=0,margin=65]}
\<close>
oops

(*
THIS IS THE ATTACK!
Level 8
!!evs. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
       \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow>
           Nonce NB \<notin> analz (spies evs)
1. !!C B' evs3.
       \<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public
        Says A C (Crypt (pubEK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
        Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
        C \<in> bad;
        Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3;
        Nonce NB \<notin> analz (spies evs3)\<rbrakk>
       \<Longrightarrow> False
*)

end

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.