Theory OtwayRees_AN

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

sectionThe Otway-Rees Protocol as Modified by Abadi and Needham

theory OtwayRees_AN imports Public begin

text
This simplified version has minimal encryption and explicit messages.

Note that the formalization does not even assume that nonces are fresh.
This is because the protocol does not rely on uniqueness of nonces for
security, only for freshness, and the proof script does not prove freshness
properties.

From page 11 of
  Abadi and Needham (1996).  
  Prudent Engineering Practice for Cryptographic Protocols.
  IEEE Trans. SE 22 (1)


inductive_set otway :: "event list set"
  where
   Nil: ― ‹The empty trace
        "[]  otway"

 | Fake: ― ‹The Spy may say anything he can say.  The sender field is correct,
            but agents don't use that information.
         "[| evsf  otway;  X  synth (analz (knows Spy evsf)) |]
          ==> Says Spy B X  # evsf  otway"

        
 | Reception: ― ‹A message that has been sent can be received by the
                  intended recipient.
              "[| evsr  otway;  Says A B X set evsr |]
               ==> Gets B X # evsr  otway"

 | OR1:  ― ‹Alice initiates a protocol run
         "evs1  otway
          ==> Says A B Agent A, Agent B, Nonce NA # evs1  otway"

 | OR2:  ― ‹Bob's response to Alice's message.
         "[| evs2  otway;
             Gets B Agent A, Agent B, Nonce NA set evs2 |]
          ==> Says B Server Agent A, Agent B, Nonce NA, Nonce NB
                 # evs2  otway"

 | OR3:  ― ‹The Server receives Bob's message.  Then he sends a new
           session key to Bob with a packet for forwarding to Alice.
         "[| evs3  otway;  Key KAB  used evs3;
             Gets Server Agent A, Agent B, Nonce NA, Nonce NB
               set evs3 |]
          ==> Says Server B
               Crypt (shrK A) Nonce NA, Agent A, Agent B, Key KAB,
                 Crypt (shrK B) Nonce NB, Agent A, Agent B, Key KAB
              # evs3  otway"

 | OR4:  ― ‹Bob receives the Server's (?) message and compares the Nonces with
             those in the message he previously sent the Server.
             Need termB  Server because we allow messages to self.
         "[| evs4  otway;  B  Server;
             Says B Server Agent A, Agent B, Nonce NA, Nonce NB set evs4;
             Gets B X, Crypt(shrK B)Nonce NB,Agent A,Agent B,Key K
               set evs4 |]
          ==> Says B A X # evs4  otway"

 | Oops: ― ‹This message models possible leaks of session keys.  The nonces
             identify the protocol run.
         "[| evso  otway;
             Says Server B
                      Crypt (shrK A) Nonce NA, Agent A, Agent B, Key K,
                        Crypt (shrK B) Nonce NB, Agent A, Agent B, Key K
               set evso |]
          ==> Notes Spy Nonce NA, Nonce NB, Key K # evso  otway"


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


textA "possibility property": there are traces that reach the end
lemma "[| B  Server; Key K  used [] |]
      ==> evs  otway.
           Says B A (Crypt (shrK A) Nonce NA, Agent A, Agent B, 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"
by (erule rev_mp, erule otway.induct, auto)



textFor reasoning about the encrypted portion of messages

lemma OR4_analz_knows_Spy:
     "[| Gets B X, Crypt(shrK B) X'  set evs;  evs  otway |]
      ==> X  analz (knows Spy evs)"
by blast


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

textSpy 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, 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)


subsectionProofs involving analz

textDescribes the form of K and NA when the Server sends this message.
lemma Says_Server_message_form:
     "[| Says Server B
            Crypt (shrK A) NA, Agent A, Agent B, Key K,
              Crypt (shrK B) NB, Agent A, Agent B, Key K
            set evs;
         evs  otway |]
      ==> K  range shrK  (i. NA = Nonce i)  (j. NB = Nonce j)"
apply (erule rev_mp)
apply (erule otway.induct, auto)
done



(****
 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.
****)


textSession 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  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, 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)


textThe Key K uniquely identifies the Server's message.
lemma unique_session_keys:
     "[| Says Server B
          Crypt (shrK A) NA, Agent A, Agent B, K,
            Crypt (shrK B) NB, Agent A, Agent B, K
          set evs;
        Says Server B'
          Crypt (shrK A') NA', Agent A', Agent B', K,
            Crypt (shrK B') NB', Agent A', Agent B', K
          set evs;
        evs  otway |]
     ==> A=A'  B=B'  NA=NA'  NB=NB'"
apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all)
apply blast+  ― ‹OR3 and OR4
done


subsectionAuthenticity properties relating to NA

textIf the encrypted message appears then it originated with the Server!
lemma NA_Crypt_imp_Server_msg [rule_format]:
    "[| A  bad;  A  B;  evs  otway |]
     ==> Crypt (shrK A) NA, Agent A, Agent B, Key K  parts (knows Spy evs)
        (NB. Says Server B
                    Crypt (shrK A) NA, Agent A, Agent B, Key K,
                      Crypt (shrK B) NB, Agent A, Agent B, Key K
                     set evs)"
apply (erule otway.induct, force)
apply (simp_all add: ex_disj_distrib)
apply blast+  ― ‹Fake, OR3
done


textCorollary: if A receives B's OR4 message then it originated with the
      Server. Freshness may be inferred from nonce NA.
lemma A_trusts_OR4:
     "[| Says B' A (Crypt (shrK A) NA, Agent A, Agent B, Key K)  set evs;
         A  bad;  A  B;  evs  otway |]
      ==> NB. Says Server B
                  Crypt (shrK A) NA, Agent A, Agent B, Key K,
                    Crypt (shrK B) NB, Agent A, Agent B, Key K
                  set evs"
by (blast intro!: NA_Crypt_imp_Server_msg)


textCrucial 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
           Crypt (shrK A) NA, Agent A, Agent B, Key K,
             Crypt (shrK B) NB, Agent A, Agent B, Key K
           set evs 
          Notes Spy NA, NB, Key K  set evs 
          Key K  analz (knows Spy evs)"
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
apply spy_analz  ― ‹Fake
apply (blast dest: unique_session_keys)+  ― ‹OR3, OR4, Oops
done


lemma Spy_not_see_encrypted_key:
     "[| Says Server B
            Crypt (shrK A) NA, Agent A, Agent B, Key K,
              Crypt (shrK B) NB, Agent A, Agent B, 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 (metis secrecy_lemma)


textA's guarantee.  The Oops premise quantifies over NB because A cannot know
  what it is.
lemma A_gets_good_key:
     "[| Says B' A (Crypt (shrK A) NA, Agent A, Agent B, Key K)  set evs;
         NB. Notes Spy NA, NB, Key K  set evs;
         A  bad;  B  bad;  A  B;  evs  otway |]
      ==> Key K  analz (knows Spy evs)"
  by (metis A_trusts_OR4 secrecy_lemma)



subsectionAuthenticity properties relating to NB

textIf the encrypted message appears then it originated with the Server!
lemma NB_Crypt_imp_Server_msg [rule_format]:
 "[| B  bad;  A  B;  evs  otway |]
  ==> Crypt (shrK B) NB, Agent A, Agent B, Key K  parts (knows Spy evs)
       (NA. Says Server B
                   Crypt (shrK A) NA, Agent A, Agent B, Key K,
                     Crypt (shrK B) NB, Agent A, Agent B, Key K
                    set evs)"
apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
apply blast+  ― ‹Fake, OR3
done



textGuarantee for B: if it gets a well-formed certificate then the Server
  has sent the correct message in round 3.
lemma B_trusts_OR3:
     "[| Says S B X, Crypt (shrK B) NB, Agent A, Agent B, Key K
            set evs;
         B  bad;  A  B;  evs  otway |]
      ==> NA. Says Server B
                   Crypt (shrK A) NA, Agent A, Agent B, Key K,
                     Crypt (shrK B) NB, Agent A, Agent B, Key K
                    set evs"
by (blast intro!: NB_Crypt_imp_Server_msg)


textThe obvious combination of B_trusts_OR3› with 
      Spy_not_see_encrypted_key›
lemma B_gets_good_key:
     "[| Gets B X, Crypt (shrK B) NB, Agent A, Agent B, Key K
           set evs;
         NA. Notes Spy NA, NB, Key K  set evs;
         A  bad;  B  bad;  A  B;  evs  otway |]
      ==> Key K  analz (knows Spy evs)"
by (blast dest: B_trusts_OR3 Spy_not_see_encrypted_key)

end