Theory NS_Shared

(*  Title:      HOL/Auth/NS_Shared.thy
    Author:     Lawrence C Paulson and Giampaolo Bella 
    Copyright   1996  University of Cambridge
*)

sectionNeedham-Schroeder Shared-Key Protocol and the Issues Property

theory NS_Shared imports Public begin

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


definition
 (* A is the true creator of X if she has sent X and X never appeared on
    the trace before this event. Recall that traces grow from head. *)
  Issues :: "[agent, agent, msg, event list]  bool"
             ("_ Issues _ with _ on _") where
   "A Issues B with X on evs =
      (Y. Says A B Y  set evs  X  parts {Y} 
        X  parts (spies (takeWhile (λz. z   Says A B Y) (rev evs))))"


inductive_set ns_shared :: "event list set"
 where
        (*Initial trace is empty*)
  Nil:  "[]  ns_shared"
        (*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_shared;  X  synth (analz (spies evsf))
          Says Spy B X # evsf  ns_shared"

        (*Alice initiates a protocol run, requesting to talk to any B*)
| NS1:  "evs1  ns_shared;  Nonce NA  used evs1
          Says A Server Agent A, Agent B, Nonce NA # evs1    ns_shared"

        (*Server's response to Alice's message.
          !! It may respond more than once to A's request !!
          Server doesn't know who the true sender is, hence the A' in
              the sender field.*)
| NS2:  "evs2  ns_shared;  Key KAB  used evs2;  KAB  symKeys;
          Says A' Server Agent A, Agent B, Nonce NA  set evs2
          Says Server A
               (Crypt (shrK A)
                  Nonce NA, Agent B, Key KAB,
                    (Crypt (shrK B) Key KAB, Agent A))
               # evs2  ns_shared"

         (*We can't assume S=Server.  Agent A "remembers" her nonce.
           Need A ≠ Server because we allow messages to self.*)
| NS3:  "evs3  ns_shared;  A  Server;
          Says S A (Crypt (shrK A) Nonce NA, Agent B, Key K, X)  set evs3;
          Says A Server Agent A, Agent B, Nonce NA  set evs3
          Says A B X # evs3  ns_shared"

        (*Bob's nonce exchange.  He does not know who the message came
          from, but responds to A because she is mentioned inside.*)
| NS4:  "evs4  ns_shared;  Nonce NB  used evs4;  K  symKeys;
          Says A' B (Crypt (shrK B) Key K, Agent A)  set evs4
          Says B A (Crypt K (Nonce NB)) # evs4  ns_shared"

        (*Alice responds with Nonce NB if she has seen the key before.
          Maybe should somehow check Nonce NA again.
          We do NOT send NB-1 or similar as the Spy cannot spoof such things.
          Letting the Spy add or subtract 1 lets him send all nonces.
          Instead we distinguish the messages by sending the nonce twice.*)
| NS5:  "evs5  ns_shared;  K  symKeys;
          Says B' A (Crypt K (Nonce NB))  set evs5;
          Says S  A (Crypt (shrK A) Nonce NA, Agent B, Key K, X)
             set evs5
          Says A B (Crypt K Nonce NB, Nonce NB) # evs5  ns_shared"

        (*This message models possible leaks of session keys.
          The two Nonces identify the protocol run: the rule insists upon
          the true senders in order to make them accurate.*)
| Oops: "evso  ns_shared;  Says B A (Crypt K (Nonce NB))  set evso;
          Says Server A (Crypt (shrK A) Nonce NA, Agent B, Key K, X)
               set evso
          Notes Spy Nonce NA, Nonce NB, Key K # evso  ns_shared"


declare Says_imp_knows_Spy [THEN parts.Inj, dest]
declare parts.Body  [dest]
declare Fake_parts_insert_in_Un  [dest]
declare analz_into_parts [dest]


textA "possibility property": there are traces that reach the end
lemma "[| A  Server; Key K  used []; K  symKeys |]
       ==> N. evs  ns_shared.
                    Says A B (Crypt K Nonce N, Nonce N)  set evs"
apply (intro exI bexI)
apply (rule_tac [2] ns_shared.Nil
       [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
        THEN ns_shared.NS4, THEN ns_shared.NS5])
apply (possibility, simp add: used_Cons)
done

(*This version is similar, while instantiating ?K and ?N to epsilon-terms
lemma "A ≠ Server ⟹ ∃evs ∈ ns_shared.
                Says A B (Crypt ?K ⦃Nonce ?N, Nonce ?N⦄) ∈ set evs"
*)


subsectionInductive proofs about termns_shared

subsubsectionForwarding lemmas, to aid simplification

textFor reasoning about the encrypted portion of message NS3
lemma NS3_msg_in_parts_spies:
     "Says S A (Crypt KA N, B, K, X)  set evs  X  parts (spies evs)"
by blast

textFor reasoning about the Oops message
lemma Oops_parts_spies:
     "Says Server A (Crypt (shrK A) NA, B, K, X)  set evs
             K  parts (spies evs)"
by blast

textTheorems of the form termX  parts (spies evs) imply that NOBODY
    sends messages containing termX

textSpy never sees another agent's shared key! (unless it's bad at start)
lemma Spy_see_shrK [simp]:
     "evs  ns_shared  (Key (shrK A)  parts (spies evs)) = (A  bad)"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
done

lemma Spy_analz_shrK [simp]:
     "evs  ns_shared  (Key (shrK A)  analz (spies evs)) = (A  bad)"
by auto


textNobody can have used non-existent keys!
lemma new_keys_not_used [simp]:
    "[|Key K  used evs; K  symKeys; evs  ns_shared|]
     ==> K  keysFor (parts (spies evs))"
apply (erule rev_mp)
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
txtFake, NS2, NS4, NS5
apply (force dest!: keysFor_parts_insert, blast+)
done


subsubsectionLemmas concerning the form of items passed in messages

textDescribes the form of K, X and K' when the Server sends this message.
lemma Says_Server_message_form:
     "Says Server A (Crypt K' N, Agent B, Key K, X)  set evs;
       evs  ns_shared
       K  range shrK 
          X = (Crypt (shrK B) Key K, Agent A) 
          K' = shrK A"
by (erule rev_mp, erule ns_shared.induct, auto)


textIf the encrypted message appears then it originated with the Server
lemma A_trusts_NS2:
     "Crypt (shrK A) NA, Agent B, Key K, X  parts (spies evs);
       A  bad;  evs  ns_shared
       Says Server A (Crypt (shrK A) NA, Agent B, Key K, X)  set evs"
apply (erule rev_mp)
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
done

lemma cert_A_form:
     "Crypt (shrK A) NA, Agent B, Key K, X  parts (spies evs);
       A  bad;  evs  ns_shared
       K  range shrK   X = (Crypt (shrK B) Key K, Agent A)"
by (blast dest!: A_trusts_NS2 Says_Server_message_form)

textEITHER describes the form of X when the following message is sent,
  OR     reduces it to the Fake case.
  Use Says_Server_message_form› if applicable.
lemma Says_S_message_form:
     "Says S A (Crypt (shrK A) Nonce NA, Agent B, Key K, X)  set evs;
       evs  ns_shared
       (K  range shrK  X = (Crypt (shrK B) Key K, Agent A))
           X  analz (spies evs)"
by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)


(*Alternative version also provable
lemma Says_S_message_form2:
  "⟦Says S A (Crypt (shrK A) ⦃Nonce NA, Agent B, Key K, X⦄) ∈ set evs;
    evs ∈ ns_shared⟧
   ⟹ Says Server A (Crypt (shrK A) ⦃Nonce NA, Agent B, Key K, X⦄) ∈ set evs
       ∨ X ∈ analz (spies evs)"
apply (case_tac "A ∈ bad")
apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
*)


(****
 SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form

  Key K ∈ analz (insert (Key KAB) (spies evs)) ⟹
  Key K ∈ analz (spies evs)

 A more general formula must be proved inductively.
****)

textNOT useful in this form, but it says that session keys are not used
  to encrypt messages containing other keys, in the actual protocol.
  We require that agents should behave like this subsequently also.
lemma  "evs  ns_shared;  Kab  range shrK 
         (Crypt KAB X)  parts (spies evs) 
         Key K  parts {X}  Key K  parts (spies evs)"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
txtFake
apply (blast dest: parts_insert_subset_Un)
txtBase, NS4 and NS5
apply auto
done


subsubsectionSession keys are not used to encrypt other session keys

textThe equality makes the induction hypothesis easier to apply

lemma analz_image_freshK [rule_format]:
 "evs  ns_shared 
   K KK. KK  - (range shrK) 
             (Key K  analz (Key`KK  (spies evs))) =
             (K  KK  Key K  analz (spies evs))"
apply (erule ns_shared.induct)
apply (drule_tac [8] Says_Server_message_form)
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
txtNS2, NS3
apply blast+ 
done


lemma analz_insert_freshK:
     "evs  ns_shared;  KAB  range shrK 
       (Key K  analz (insert (Key KAB) (spies evs))) =
       (K = KAB  Key K  analz (spies evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)


subsubsectionThe session key K uniquely identifies the message

textIn messages of this form, the session key uniquely identifies the rest
lemma unique_session_keys:
     "Says Server A (Crypt (shrK A) NA, Agent B, Key K, X)  set evs;
       Says Server A' (Crypt (shrK A') NA', Agent B', Key K, X')  set evs;
       evs  ns_shared  A=A'  NA=NA'  B=B'  X = X'"
by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)


subsubsectionCrucial secrecy property: Spy doesn't see the keys sent in NS2

textBeware of [rule_format]› and the universal quantifier!
lemma secrecy_lemma:
     "Says Server A (Crypt (shrK A) NA, Agent B, Key K,
                                      Crypt (shrK B) Key K, Agent A)
               set evs;
         A  bad;  B  bad;  evs  ns_shared
       (NB. Notes Spy NA, NB, Key K  set evs) 
         Key K  analz (spies evs)"
apply (erule rev_mp)
apply (erule ns_shared.induct, force)
apply (frule_tac [7] Says_Server_message_form)
apply (frule_tac [4] Says_S_message_form)
apply (erule_tac [5] disjE)
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
txtNS2
apply blast
txtNS3
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
             dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
txtOops
apply (blast dest: unique_session_keys)
done



textFinal version: Server's message in the most abstract form
lemma Spy_not_see_encrypted_key:
     "Says Server A (Crypt K' NA, Agent B, Key K, X)  set evs;
       NB. Notes Spy NA, NB, Key K  set evs;
       A  bad;  B  bad;  evs  ns_shared
       Key K  analz (spies evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)


subsectionGuarantees available at various stages of protocol

textIf the encrypted message appears then it originated with the Server
lemma B_trusts_NS3:
     "Crypt (shrK B) Key K, Agent A  parts (spies evs);
       B  bad;  evs  ns_shared
       NA. Says Server A
               (Crypt (shrK A) NA, Agent B, Key K,
                                 Crypt (shrK B) Key K, Agent A)
               set evs"
apply (erule rev_mp)
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
done


lemma A_trusts_NS4_lemma [rule_format]:
   "evs  ns_shared 
      Key K  analz (spies evs) 
      Says Server A (Crypt (shrK A) NA, Agent B, Key K, X)  set evs 
      Crypt K (Nonce NB)  parts (spies evs) 
      Says B A (Crypt K (Nonce NB))  set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
apply (analz_mono_contra, simp_all, blast)
txtNS2: contradiction from the assumptions termKey K  used evs2 and
    termCrypt K (Nonce NB)  parts (spies evs2) 
apply (force dest!: Crypt_imp_keysFor)
txtNS4
apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
done

textThis version no longer assumes that K is secure
lemma A_trusts_NS4:
     "Crypt K (Nonce NB)  parts (spies evs);
       Crypt (shrK A) NA, Agent B, Key K, X  parts (spies evs);
       NB. Notes Spy NA, NB, Key K  set evs;
       A  bad;  B  bad;  evs  ns_shared
       Says B A (Crypt K (Nonce NB))  set evs"
by (blast intro: A_trusts_NS4_lemma
          dest: A_trusts_NS2 Spy_not_see_encrypted_key)

textIf the session key has been used in NS4 then somebody has forwarded
  component X in some instance of NS4.  Perhaps an interesting property,
  but not needed (after all) for the proofs below.
theorem NS4_implies_NS3 [rule_format]:
  "evs  ns_shared 
     Key K  analz (spies evs) 
     Says Server A (Crypt (shrK A) NA, Agent B, Key K, X)  set evs 
     Crypt K (Nonce NB)  parts (spies evs) 
     (A'. Says A' B X  set evs)"
apply (erule ns_shared.induct, force)
apply (drule_tac [4] NS3_msg_in_parts_spies)
apply analz_mono_contra
apply (simp_all add: ex_disj_distrib, blast)
txtNS2
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
txtNS4
apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
done


lemma B_trusts_NS5_lemma [rule_format]:
  "B  bad;  evs  ns_shared 
     Key K  analz (spies evs) 
     Says Server A
          (Crypt (shrK A) NA, Agent B, Key K,
                            Crypt (shrK B) Key K, Agent A)  set evs 
     Crypt K Nonce NB, Nonce NB  parts (spies evs) 
     Says A B (Crypt K Nonce NB, Nonce NB)  set evs"
apply (erule ns_shared.induct, force)
apply (drule_tac [4] NS3_msg_in_parts_spies)
apply (analz_mono_contra, simp_all, blast)
txtNS2
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
txtNS5
apply (blast dest!: A_trusts_NS2
             dest: Says_imp_knows_Spy [THEN analz.Inj]
                   unique_session_keys Crypt_Spy_analz_bad)
done


textVery strong Oops condition reveals protocol's weakness
lemma B_trusts_NS5:
     "Crypt K Nonce NB, Nonce NB  parts (spies evs);
       Crypt (shrK B) Key K, Agent A  parts (spies evs);
       NA NB. Notes Spy NA, NB, Key K  set evs;
       A  bad;  B  bad;  evs  ns_shared
       Says A B (Crypt K Nonce NB, Nonce NB)  set evs"
by (blast intro: B_trusts_NS5_lemma
          dest: B_trusts_NS3 Spy_not_see_encrypted_key)

textUnaltered so far wrt original version

subsectionLemmas for reasoning about predicate "Issues"

lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done

lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done

lemma spies_Notes_rev: "spies (evs @ [Notes A X]) =
          (if Abad then insert X (spies evs) else spies evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
done

lemma spies_evs_rev: "spies evs = spies (rev evs)"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a")
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev)
done

lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono]

lemma spies_takeWhile: "spies (takeWhile P evs)  spies evs"
apply (induct_tac "evs")
apply (rename_tac [2] a b)
apply (induct_tac [2] "a", auto)
txtResembles used_subset_append› in theory Event.
done

lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono]


subsectionGuarantees of non-injective agreement on the session key, and
of key distribution. They also express forms of freshness of certain messages,
namely that agents were alive after something happened.

lemma B_Issues_A:
     " Says B A (Crypt K (Nonce Nb))  set evs;
         Key K  analz (spies evs);
         A  bad;  B  bad; evs  ns_shared 
       B Issues A with (Crypt K (Nonce Nb)) on evs"
apply (simp (no_asm) add: Issues_def)
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule ns_shared.induct, analz_mono_contra)
apply (simp_all)
txtfake
apply blast
apply (simp_all add: takeWhile_tail)
txtNS3 remains by pure coincidence!
apply (force dest!: A_trusts_NS2 Says_Server_message_form)
txtNS4 would be the non-trivial case can be solved by Nb being used
apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD]
                   parts_spies_evs_revD2 [THEN subsetD])
done

textTells A that B was alive after she sent him the session key.  The
session key must be assumed confidential for this deduction to be meaningful,
but that assumption can be relaxed by the appropriate argument.

Precisely, the theorem guarantees (to A) key distribution of the session key
to B. It also guarantees (to A) non-injective agreement of B with A on the
session key. Both goals are available to A in the sense of Goal Availability.

lemma A_authenticates_and_keydist_to_B:
     "Crypt K (Nonce NB)  parts (spies evs);
       Crypt (shrK A) NA, Agent B, Key K, X  parts (spies evs);
       Key K  analz(knows Spy evs);
       A  bad;  B  bad;  evs  ns_shared
       B Issues A with (Crypt K (Nonce NB)) on evs"
by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2)

lemma A_trusts_NS5:
  " Crypt K Nonce NB, Nonce NB  parts(spies evs);
     Crypt (shrK A) Nonce NA, Agent B, Key K, X  parts(spies evs);
     Key K  analz (spies evs);
     A  bad; B  bad; evs  ns_shared 
  Says A B (Crypt K Nonce NB, Nonce NB)  set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule ns_shared.induct, analz_mono_contra)
apply (simp_all)
txtFake
apply blast
txtNS2
apply (force dest!: Crypt_imp_keysFor)
txtNS3
apply (metis NS3_msg_in_parts_spies parts_cut_eq)
txtNS5, the most important case, can be solved by unicity
apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
done

lemma A_Issues_B:
     " Says A B (Crypt K Nonce NB, Nonce NB)  set evs;
        Key K  analz (spies evs);
        A  bad;  B  bad; evs  ns_shared 
     A Issues B with (Crypt K Nonce NB, Nonce NB) on evs"
apply (simp (no_asm) add: Issues_def)
apply (rule exI)
apply (rule conjI, assumption)
apply (simp (no_asm))
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule ns_shared.induct, analz_mono_contra)
apply (simp_all)
txtfake
apply blast
apply (simp_all add: takeWhile_tail)
txtNS3 remains by pure coincidence!
apply (force dest!: A_trusts_NS2 Says_Server_message_form)
txtNS5 is the non-trivial case and cannot be solved as in termB_Issues_A! because NB is not fresh. We need termA_trusts_NS5, proved for this very purpose
apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD]
        parts_spies_evs_revD2 [THEN subsetD])
done

textTells B that A was alive after B issued NB.

Precisely, the theorem guarantees (to B) key distribution of the session key to A. It also guarantees (to B) non-injective agreement of A with B on the session key. Both goals are available to B in the sense of Goal Availability.

lemma B_authenticates_and_keydist_to_A:
     "Crypt K Nonce NB, Nonce NB  parts (spies evs);
       Crypt (shrK B) Key K, Agent A  parts (spies evs);
       Key K  analz (spies evs);
       A  bad;  B  bad;  evs  ns_shared
    A Issues B with (Crypt K Nonce NB, Nonce NB) on evs"
by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3)

end