Theory OtwayRees

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

section‹The Original Otway-Rees Protocol›

theory OtwayRees imports Public begin

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

This is the original version, which encrypts Nonce NB.›

inductive_set otway :: "event list set"
  where
   Nil:  "[]  otway"
   ― ‹Initial trace is empty›
 | Fake: "evsf  otway;  X  synth (analz (knows Spy evsf)) 
           Says Spy B X  # evsf  otway"
   ― ‹The spy can say almost anything.›
 | Reception: "evsr  otway;  Says A B X set evsr  Gets B X # evsr  otway"
   ― ‹A message that has been sent can be received by the intended recipient.›
 | OR1:  "evs1  otway;  Nonce NA  used evs1
           Says A B Nonce NA, Agent A, Agent B,
                         Crypt (shrK A) Nonce NA, Agent A, Agent B 
                 # evs1  otway"
  ― ‹Alice initiates a protocol run›
 | OR2:  "evs2  otway;  Nonce NB  used evs2;
             Gets B Nonce NA, Agent A, Agent B, X  set evs2
           Says B Server
                  Nonce NA, Agent A, Agent B, X,
                    Crypt (shrK B)
                      Nonce NA, Nonce NB, Agent A, Agent B
                 # evs2  otway"
   ― ‹Bob's response to Alice's message.  Note that NB is encrypted.›
 | OR3:  "evs3  otway;  Key KAB  used evs3;
             Gets Server
                  Nonce NA, Agent A, Agent B,
                    Crypt (shrK A) Nonce NA, Agent A, Agent B,
                    Crypt (shrK B) Nonce NA, Nonce NB, Agent A, Agent B
                set evs3
           Says Server B
                  Nonce NA,
                    Crypt (shrK A) Nonce NA, Key KAB,
                    Crypt (shrK B) Nonce NB, Key KAB
                 # evs3  otway"
   ― ‹The Server receives Bob's message and checks that the three NAs
       match.  Then he sends a new session key to Bob with a packet for forwarding to Alice›
 | OR4:  "evs4  otway;  B  Server;
             Says B Server Nonce NA, Agent A, Agent B, X',
                             Crypt (shrK B)
                                   Nonce NA, Nonce NB, Agent A, Agent B
                set evs4;
             Gets B Nonce NA, X, Crypt (shrK B) Nonce NB, Key K
                set evs4
           Says B A Nonce NA, X # evs4  otway"
   ― ‹Bob receives the Server's (?) message and compares the Nonces with
       those in the message he previously sent the Server.
       Need @{term"B  Server"} because we allow messages to self.›
 | Oops: "evso  otway;
             Says Server B Nonce NA, X, Crypt (shrK B) Nonce NB, Key K
                set evso
           Notes Spy Nonce NA, Nonce NB, Key K # evso  otway"
   ― ‹This message models possible leaks of session keys.  The nonces identify the protocol run›

declare Says_imp_analz_Spy [dest]
declare parts.Body  [dest]
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un  [dest]


text‹A "possibility property": there are traces that reach the end›
lemma "B  Server; Key K  used []
       evs  otway.
             Says B A Nonce NA, Crypt (shrK A) Nonce NA, Key K
                set evs"
apply (intro exI bexI)
apply (rule_tac [2] otway.Nil
                    [THEN otway.OR1, THEN otway.Reception,
                     THEN otway.OR2, THEN otway.Reception,
                     THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) 
apply (possibility, simp add: used_Cons) 
done

lemma Gets_imp_Says [dest!]:
     "Gets B X  set evs; evs  otway  A. Says A B X  set evs"
apply (erule rev_mp)
apply (erule otway.induct, auto)
done


(** For reasoning about the encrypted portion of messages **)

lemma OR2_analz_knows_Spy:
     "Gets B N, Agent A, Agent B, X  set evs;  evs  otway
       X  analz (knows Spy evs)"
  by blast

lemma OR4_analz_knows_Spy:
     "Gets B N, X, Crypt (shrK B) X'  set evs;  evs  otway
       X  analz (knows Spy evs)"
  by blast

(*These lemmas assist simplification by removing forwarded X-variables.
  We can replace them by rewriting with parts_insert2 and proving using
  dest: parts_cut, but the proofs become more difficult.*)
lemmas OR2_parts_knows_Spy =
    OR2_analz_knows_Spy [THEN analz_into_parts]

(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
  some reason proofs work without them!*)


text‹Theorems of the form termX  parts (spies evs) imply that
NOBODY sends messages containing X!›

text‹Spy never sees a good agent's shared key!›
lemma Spy_see_shrK [simp]:
     "evs  otway  (Key (shrK A)  parts (knows Spy evs)) = (A  bad)"
by (erule otway.induct, force,
    drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)


lemma Spy_analz_shrK [simp]:
     "evs  otway  (Key (shrK A)  analz (knows Spy evs)) = (A  bad)"
by auto

lemma Spy_see_shrK_D [dest!]:
     "Key (shrK A)  parts (knows Spy evs);  evs  otway  A  bad"
by (blast dest: Spy_see_shrK)


subsection‹Towards Secrecy: Proofs Involving termanalz

text ‹Describes the form of K and NA when the Server sends this message.  Also
  for Oops case.›
lemma Says_Server_message_form:
     "Says Server B NA, X, Crypt (shrK B) NB, Key K  set evs;
         evs  otway
       K  range shrK  (i. NA = Nonce i)  (j. NB = Nonce j)"
by (erule rev_mp, erule otway.induct, simp_all)


(****
 The following is to prove theorems of the form

  Key K ∈ analz (insert (Key KAB) (knows Spy evs)) ⟹
  Key K ∈ analz (knows Spy evs)

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


text‹Session keys are not used to encrypt other session keys›

text‹The equality makes the induction hypothesis easier to apply›
lemma analz_image_freshK [rule_format]:
 "evs  otway 
   K KK. KK  -(range shrK) 
          (Key K  analz (Key`KK  (knows Spy evs))) =
          (K  KK | Key K  analz (knows Spy evs))"
apply (erule otway.induct)
apply (frule_tac [8] Says_Server_message_form)
apply (drule_tac [7] OR4_analz_knows_Spy)
apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) 
done

lemma analz_insert_freshK:
  "evs  otway;  KAB  range shrK 
      (Key K  analz (insert (Key KAB) (knows Spy evs))) =
      (K = KAB | Key K  analz (knows Spy evs))"
by (simp only: analz_image_freshK analz_image_freshK_simps)


text‹The Key K uniquely identifies the Server's  message.›
lemma unique_session_keys:
     "Says Server B NA, X, Crypt (shrK B) NB, K    set evs;
         Says Server B' NA',X',Crypt (shrK B') NB',K  set evs;
         evs  otway  X=X'  B=B'  NA=NA'  NB=NB'"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
apply blast+  ― ‹OR3 and OR4›
done


subsection‹Authenticity properties relating to NA›

text‹Only OR1 can have caused such a part of a message to appear.›
lemma Crypt_imp_OR1 [rule_format]:
 "A  bad;  evs  otway
   Crypt (shrK A) NA, Agent A, Agent B  parts (knows Spy evs) 
      Says A B NA, Agent A, Agent B,
                 Crypt (shrK A) NA, Agent A, Agent B
         set evs"
by (erule otway.induct, force,
    drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)

lemma Crypt_imp_OR1_Gets:
     "Gets B NA, Agent A, Agent B,
                  Crypt (shrK A) NA, Agent A, Agent B  set evs;
         A  bad; evs  otway
        Says A B NA, Agent A, Agent B,
                      Crypt (shrK A) NA, Agent A, Agent B
              set evs"
by (blast dest: Crypt_imp_OR1)


text‹The Nonce NA uniquely identifies A's message›
lemma unique_NA:
     "Crypt (shrK A) NA, Agent A, Agent B  parts (knows Spy evs);
         Crypt (shrK A) NA, Agent A, Agent C  parts (knows Spy evs);
         evs  otway;  A  bad
       B = C"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done


text‹It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
  OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
  over-simplified version of this protocol: see OtwayRees_Bad›.›
lemma no_nonce_OR1_OR2:
   "Crypt (shrK A) NA, Agent A, Agent B  parts (knows Spy evs);
       A  bad;  evs  otway
     Crypt (shrK A) NA', NA, Agent A', Agent A  parts (knows Spy evs)"
apply (erule rev_mp)
apply (erule otway.induct, force,
       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done

text‹Crucial property: If the encrypted message appears, and A has used NA
  to start a run, then it originated with the Server!›
lemma NA_Crypt_imp_Server_msg [rule_format]:
     "A  bad;  evs  otway
       Says A B NA, Agent A, Agent B,
                     Crypt (shrK A) NA, Agent A, Agent B  set evs 
          Crypt (shrK A) NA, Key K  parts (knows Spy evs)
           (NB. Says Server B
                         NA,
                           Crypt (shrK A) NA, Key K,
                           Crypt (shrK B) NB, Key K  set evs)"
apply (erule otway.induct, force,
       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
  subgoal ― ‹OR1: by freshness›
    by blast  
  subgoal ― ‹OR3›
    by (blast dest!: no_nonce_OR1_OR2 intro: unique_NA)
  subgoal ― ‹OR4›
    by (blast intro!: Crypt_imp_OR1) 
done


text‹Corollary: if A receives B's OR4 message and the nonce NA agrees
  then the key really did come from the Server!  CANNOT prove this of the
  bad form of this protocol, even though we can prove
  Spy_not_see_encrypted_key›
lemma A_trusts_OR4:
     "Says A  B NA, Agent A, Agent B,
                     Crypt (shrK A) NA, Agent A, Agent B  set evs;
         Says B' A NA, Crypt (shrK A) NA, Key K  set evs;
     A  bad;  evs  otway
   NB. Says Server B
               NA,
                 Crypt (shrK A) NA, Key K,
                 Crypt (shrK B) NB, Key K
                  set evs"
by (blast intro!: NA_Crypt_imp_Server_msg)


text‹Crucial secrecy property: Spy does not see the keys sent in msg OR3
    Does not in itself guarantee security: an attack could violate
    the premises, e.g. by having termA=Spy
lemma secrecy_lemma:
 "A  bad;  B  bad;  evs  otway
   Says Server B
        NA, Crypt (shrK A) NA, Key K,
          Crypt (shrK B) NB, Key K  set evs 
      Notes Spy NA, NB, Key K  set evs 
      Key K  analz (knows Spy evs)"
  apply (erule otway.induct, force, simp_all)
  subgoal ― ‹Fake›
    by spy_analz
  subgoal ― ‹OR2›
    by (drule OR2_analz_knows_Spy) (auto simp: analz_insert_eq)
  subgoal ― ‹OR3›
    by (auto simp add: analz_insert_freshK pushes)
  subgoal ― ‹OR4›
    by (drule OR4_analz_knows_Spy) (auto simp: analz_insert_eq)
  subgoal ― ‹Oops›
    by (auto simp add: Says_Server_message_form analz_insert_freshK unique_session_keys)
  done

theorem Spy_not_see_encrypted_key:
     "Says Server B
          NA, Crypt (shrK A) NA, Key K,
                Crypt (shrK B) NB, Key K  set evs;
         Notes Spy NA, NB, Key K  set evs;
         A  bad;  B  bad;  evs  otway
       Key K  analz (knows Spy evs)"
by (blast dest: Says_Server_message_form secrecy_lemma)

text‹This form is an immediate consequence of the previous result.  It is 
similar to the assertions established by other methods.  It is equivalent
to the previous result in that the Spy already has termanalz and
termsynth at his disposal.  However, the conclusion 
termKey K  knows Spy evs appears not to be inductive: all the cases
other than Fake are trivial, while Fake requires 
termKey K  analz (knows Spy evs).›
lemma Spy_not_know_encrypted_key:
     "Says Server B
          NA, Crypt (shrK A) NA, Key K,
                Crypt (shrK B) NB, Key K  set evs;
         Notes Spy NA, NB, Key K  set evs;
         A  bad;  B  bad;  evs  otway
       Key K  knows Spy evs"
by (blast dest: Spy_not_see_encrypted_key)


text‹A's guarantee.  The Oops premise quantifies over NB because A cannot know
  what it is.›
lemma A_gets_good_key:
     "Says A  B NA, Agent A, Agent B,
                     Crypt (shrK A) NA, Agent A, Agent B  set evs;
         Says B' A NA, Crypt (shrK A) NA, Key K  set evs;
         NB. Notes Spy NA, NB, Key K  set evs;
         A  bad;  B  bad;  evs  otway
       Key K  analz (knows Spy evs)"
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key)


subsection‹Authenticity properties relating to NB›

text‹Only OR2 can have caused such a part of a message to appear.  We do not
  know anything about X: it does NOT have to have the right form.›
lemma Crypt_imp_OR2:
     "Crypt (shrK B) NA, NB, Agent A, Agent B  parts (knows Spy evs);
         B  bad;  evs  otway
       X. Says B Server
                 NA, Agent A, Agent B, X,
                   Crypt (shrK B) NA, NB, Agent A, Agent B
                  set evs"
apply (erule rev_mp)
apply (erule otway.induct, force,
       drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done


text‹The Nonce NB uniquely identifies B's  message›
lemma unique_NB:
     "Crypt (shrK B) NA, NB, Agent A, Agent B  parts(knows Spy evs);
         Crypt (shrK B) NC, NB, Agent C, Agent B  parts(knows Spy evs);
           evs  otway;  B  bad
          NC = NA  C = A"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
       drule_tac [4] OR2_parts_knows_Spy, simp_all)
apply blast+  ― ‹Fake, OR2›
done

text‹If the encrypted message appears, and B has used Nonce NB,
  then it originated with the Server!  Quite messy proof.›
lemma NB_Crypt_imp_Server_msg [rule_format]:
 "B  bad;  evs  otway
   Crypt (shrK B) NB, Key K  parts (knows Spy evs)
       (X'. Says B Server
                     NA, Agent A, Agent B, X',
                       Crypt (shrK B) NA, NB, Agent A, Agent B
            set evs
            Says Server B
                NA, Crypt (shrK A) NA, Key K,
                      Crypt (shrK B) NB, Key K
                     set evs)"
apply simp
apply (erule otway.induct, force, simp_all)
  subgoal ― ‹Fake›
    by blast 
  subgoal ― ‹OR2›
    by (force dest!: OR2_parts_knows_Spy)
  subgoal ― ‹OR3›
    by (blast dest: unique_NB dest!: no_nonce_OR1_OR2)  ― ‹OR3›
  subgoal ― ‹OR4›
    by (blast dest!: Crypt_imp_OR2) 
done


text‹Guarantee for B: if it gets a message with matching NB then the Server
  has sent the correct message.›
theorem B_trusts_OR3:
     "Says B Server NA, Agent A, Agent B, X',
                         Crypt (shrK B) NA, NB, Agent A, Agent B
            set evs;
         Gets B NA, X, Crypt (shrK B) NB, Key K  set evs;
         B  bad;  evs  otway
       Says Server B
               NA,
                 Crypt (shrK A) NA, Key K,
                 Crypt (shrK B) NB, Key K
                  set evs"
by (blast intro!: NB_Crypt_imp_Server_msg)


text‹The obvious combination of B_trusts_OR3› with 
      Spy_not_see_encrypted_key›
lemma B_gets_good_key:
     "Says B Server NA, Agent A, Agent B, X',
                         Crypt (shrK B) NA, NB, Agent A, Agent B
            set evs;
         Gets B NA, X, Crypt (shrK B) NB, Key K  set evs;
         Notes Spy NA, NB, Key K  set evs;
         A  bad;  B  bad;  evs  otway
       Key K  analz (knows Spy evs)"
by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key)


lemma OR3_imp_OR2:
     "Says Server B
              NA, Crypt (shrK A) NA, Key K,
                Crypt (shrK B) NB, Key K  set evs;
         B  bad;  evs  otway
   X. Says B Server NA, Agent A, Agent B, X,
                            Crypt (shrK B) NA, NB, Agent A, Agent B
               set evs"
apply (erule rev_mp)
apply (erule otway.induct, simp_all)
apply (blast dest!: Crypt_imp_OR2)+
done


text‹After getting and checking OR4, agent A can trust that B has been active.
  We could probably prove that X has the expected form, but that is not
  strictly necessary for authentication.›
theorem A_auths_B:
     "Says B' A NA, Crypt (shrK A) NA, Key K  set evs;
         Says A  B NA, Agent A, Agent B,
                     Crypt (shrK A) NA, Agent A, Agent B  set evs;
         A  bad;  B  bad;  evs  otway
   NB X. Says B Server NA, Agent A, Agent B, X,
                               Crypt (shrK B)  NA, NB, Agent A, Agent B
                  set evs"
by (blast dest!: A_trusts_OR4 OR3_imp_OR2)

end