Theory OtwayReesBella

(*  Title:      HOL/Auth/OtwayReesBella.thy
    Author:     Giampaolo Bella, Catania University
*)

sectionBella's version of the Otway-Rees protocol


theory OtwayReesBella imports Public begin

textBella's modifications to a version of the Otway-Rees protocol taken from
the BAN paper only concern message 7. The updated protocol makes the goal of
key distribution of the session key available to A. Investigating the
principle of Goal Availability undermines the BAN claim about the original
protocol, that "this protocol does not make use of Kab as an encryption key,
so neither principal can know whether the key is known to the other". The
updated protocol makes no use of the session key to encrypt but informs A that
B knows it.

inductive_set orb :: "event list set"
 where

  Nil:  "[] orb"

| Fake: "evsa orb;  X synth (analz (knows Spy evsa))
          Says Spy B X  # evsa  orb"

| Reception: "evsr orb;  Says A B X  set evsr
               Gets B X # evsr  orb"

| OR1:  "evs1 orb;  Nonce NA  used evs1
          Says A B Nonce M, Agent A, Agent B, 
                   Crypt (shrK A) Nonce NA, Nonce M, Agent A, Agent B 
               # evs1  orb"

| OR2:  "evs2 orb;  Nonce NB  used evs2;
           Gets B Nonce M, Agent A, Agent B, X  set evs2
         Says B Server 
                Nonce M, Agent A, Agent B, X, 
           Crypt (shrK B) Nonce NB, Nonce M, Nonce M, Agent A, Agent B
               # evs2  orb"

| OR3:  "evs3 orb;  Key KAB  used evs3;
          Gets Server 
             Nonce M, Agent A, Agent B, 
               Crypt (shrK A) Nonce NA, Nonce M, Agent A, Agent B, 
               Crypt (shrK B) Nonce NB, Nonce M, Nonce M, Agent A, Agent B
           set evs3
         Says Server B Nonce M,
                    Crypt (shrK B) Crypt (shrK A) Nonce NA, Key KAB,
                                      Nonce NB, Key KAB
               # evs3  orb"

  (*B can only check that the message he is bouncing is a ciphertext*)
  (*Sending M back is omitted*)   
| OR4:  "evs4 orb; B  Server;  p q. X  p, q; 
          Says B Server Nonce M, Agent A, Agent B, X', 
                Crypt (shrK B) Nonce NB, Nonce M, Nonce M, Agent A, Agent B
             set evs4;
          Gets B Nonce M, Crypt (shrK B) X, Nonce NB, Key KAB
             set evs4
         Says B A Nonce M, X # evs4  orb"


| Oops: "evso orb;  
           Says Server B Nonce M,
                    Crypt (shrK B) Crypt (shrK A) Nonce NA, Key KAB,
                                      Nonce NB, Key KAB 
              set evso
  Notes Spy Agent A, Agent B, Nonce NA, Nonce NB, Key KAB # evso 
      orb"



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


textFragile proof, with backtracking in the possibility call.
lemma possibility_thm: "A  Server; B  Server; Key K  used[]    
          evs  orb.           
     Says B A Nonce M, Crypt (shrK A) Nonce Na, Key K  set evs"
apply (intro exI bexI)
apply (rule_tac [2] orb.Nil
                    [THEN orb.OR1, THEN orb.Reception,
                     THEN orb.OR2, THEN orb.Reception,
                     THEN orb.OR3, THEN orb.Reception, THEN orb.OR4]) 
apply (possibility, simp add: used_Cons)  
done


lemma Gets_imp_Says :
     "Gets B X  set evs; evs  orb  A. Says A B X  set evs"
apply (erule rev_mp)
apply (erule orb.induct)
apply auto
done

lemma Gets_imp_knows_Spy: 
     "Gets B X  set evs; evs  orb   X  knows Spy evs"
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)

declare Gets_imp_knows_Spy [THEN parts.Inj, dest]

lemma Gets_imp_knows:
     "Gets B X  set evs; evs  orb   X  knows B evs"
by (metis Gets_imp_knows_Spy Gets_imp_knows_agents)

lemma OR2_analz_knows_Spy: 
   "Gets B Nonce M, Agent A, Agent B, X  set evs; evs  orb   
     X  analz (knows Spy evs)"
by (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])

lemma OR4_parts_knows_Spy: 
   "Gets B Nonce M, Crypt (shrK B) X, Nonce Nb, Key Kab   set evs; 
      evs  orb    X  parts (knows Spy evs)"
by blast

lemma Oops_parts_knows_Spy: 
    "Says Server B Nonce M, Crypt K' X, Nonce Nb, K  set evs  
      K  parts (knows Spy evs)"
by blast

lemmas OR2_parts_knows_Spy =
    OR2_analz_knows_Spy [THEN analz_into_parts]

ML

fun parts_explicit_tac ctxt i =
    forward_tac ctxt [@{thm Oops_parts_knows_Spy}] (i+7) THEN
    forward_tac ctxt [@{thm OR4_parts_knows_Spy}]  (i+6) THEN
    forward_tac ctxt [@{thm OR2_parts_knows_Spy}]  (i+4)

 
method_setup parts_explicit = 
    Scan.succeed (SIMPLE_METHOD' o parts_explicit_tac)
  "to explicitly state that some message components belong to parts knows Spy"


lemma Spy_see_shrK [simp]: 
    "evs  orb  (Key (shrK A)  parts (knows Spy evs)) = (A  bad)"
by (erule orb.induct, parts_explicit, simp_all, blast+)

lemma Spy_analz_shrK [simp]: 
"evs  orb  (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  orb|] ==> A  bad"
by (blast dest: Spy_see_shrK)

lemma new_keys_not_used [simp]:
   "Key K  used evs; K  symKeys; evs  orb   K  keysFor (parts (knows Spy evs))"
apply (erule rev_mp)
apply (erule orb.induct, parts_explicit, simp_all)
apply (force dest!: keysFor_parts_insert)
apply (blast+)
done



subsectionProofs involving analz

textDescribes the form of K and NA when the Server sends this message.  Also
  for Oops case.
lemma Says_Server_message_form: 
"Says Server B  Nonce M, Crypt (shrK B) X, Nonce Nb, Key K  set evs;  
     evs  orb                                            
  K  range shrK  ( A Na. X=(Crypt (shrK A) Nonce Na, Key K))"
by (erule rev_mp, erule orb.induct, simp_all)

lemma Says_Server_imp_Gets: 
 "Says Server B Nonce M, Crypt (shrK B) Crypt (shrK A) Nonce Na, Key K,
                                             Nonce Nb, Key K  set evs;
    evs  orb
    Gets Server Nonce M, Agent A, Agent B, 
                   Crypt (shrK A) Nonce Na, Nonce M, Agent A, Agent B, 
               Crypt (shrK B) Nonce Nb, Nonce M, Nonce M, Agent A, Agent B
          set evs"
by (erule rev_mp, erule orb.induct, simp_all)


lemma A_trusts_OR1: 
"Crypt (shrK A) Nonce Na, Nonce M, Agent A, Agent B  parts (knows Spy evs);  
    A  bad; evs  orb                   
  Says A B Nonce M, Agent A, Agent B, Crypt (shrK A) Nonce Na, Nonce M, Agent A, Agent B  set evs"
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
apply (blast)
done


lemma B_trusts_OR2:
 "Crypt (shrK B) Nonce Nb, Nonce M, Nonce M, Agent A, Agent B  
       parts (knows Spy evs);  B  bad; evs  orb                   
   ( X. Says B Server Nonce M, Agent A, Agent B, X,  
              Crypt (shrK B) Nonce Nb, Nonce M, Nonce M, Agent A, Agent B 
           set evs)"
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
apply (blast+)
done


lemma B_trusts_OR3: 
"Crypt (shrK B) X, Nonce Nb, Key K  parts (knows Spy evs);  
   B  bad; evs  orb                   
  M. Says Server B Nonce M, Crypt (shrK B) X, Nonce Nb, Key K 
          set evs"
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
apply (blast+)
done

lemma Gets_Server_message_form: 
"Gets B Nonce M, Crypt (shrK B) X, Nonce Nb, Key K  set evs;  
    evs  orb                                              
  (K  range shrK  ( A Na. X = (Crypt (shrK A) Nonce Na, Key K)))    
             | X  analz (knows Spy evs)"
by (metis B_trusts_OR3 Crypt_Spy_analz_bad Gets_imp_Says MPair_analz MPair_parts
          Says_Server_message_form Says_imp_analz_Spy Says_imp_parts_knows_Spy)

lemma unique_Na: "Says A B  Nonce M, Agent A, Agent B, Crypt (shrK A) Nonce Na, Nonce M, Agent A, Agent B  set evs;   
         Says A B' Nonce M', Agent A, Agent B', Crypt (shrK A) Nonce Na, Nonce M', Agent A, Agent B'  set evs;  
    A  bad; evs  orb  B=B'  M=M'"
by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)

lemma unique_Nb: "Says B Server Nonce M, Agent A, Agent B, X, Crypt (shrK B) Nonce Nb, Nonce M, Nonce M, Agent A, Agent B  set evs;   
         Says B Server Nonce M', Agent A', Agent B, X', Crypt (shrK B) Nonce Nb,Nonce M', Nonce M', Agent A', Agent B  set evs;   
    B  bad; evs  orb    M=M'  A=A'  X=X'"
by (erule rev_mp, erule rev_mp, erule orb.induct, simp_all, blast+)

lemma analz_image_freshCryptK_lemma:
"(Crypt K X  analz (Key`nE  H))  (Crypt K X  analz H)   
        (Crypt K X  analz (Key`nE  H)) = (Crypt K X  analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])

ML

structure OtwayReesBella =
struct

val analz_image_freshK_ss =
  simpset_of
   (context delsimps [image_insert, image_Un]
      delsimps [@{thm imp_disjL}]    (*reduces blow-up*)
      addsimps @{thms analz_image_freshK_simps})

end


method_setup analz_freshCryptK = 
    Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD
      (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]),
          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}),
          ALLGOALS (asm_simp_tac
            (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))])))
  "for proving useful rewrite rule"


method_setup disentangle = 
    Scan.succeed
     (fn ctxt => SIMPLE_METHOD
      (REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE, disjE] 
                   ORELSE' hyp_subst_tac ctxt)))
  "for eliminating conjunctions, disjunctions and the like"



lemma analz_image_freshCryptK [rule_format]: 
"evs  orb                               
     Key K  analz (knows Spy evs)   
       ( KK. KK  - (range shrK)                   
             (Crypt K X  analz (Key`KK  (knows Spy evs))) =   
             (Crypt K X  analz (knows Spy evs)))"
apply (erule orb.induct)
apply (analz_mono_contra)
apply (frule_tac [7] Gets_Server_message_form)
apply (frule_tac [9] Says_Server_message_form)
apply disentangle
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN  analz.Snd])
prefer 8 apply clarify
apply (analz_freshCryptK, spy_analz, fastforce)
done



lemma analz_insert_freshCryptK: 
"evs  orb;  Key K  analz (knows Spy evs);  
         Seskey  range shrK    
         (Crypt K X  analz (insert (Key Seskey) (knows Spy evs))) =  
         (Crypt K X  analz (knows Spy evs))"
by (simp only: analz_image_freshCryptK analz_image_freshK_simps)


lemma analz_hard: 
"Says A B Nonce M, Agent A, Agent B,  
             Crypt (shrK A) Nonce Na, Nonce M, Agent A, Agent B set evs; 
   Crypt (shrK A) Nonce Na, Key K  analz (knows Spy evs);  
   A  bad; B  bad; evs  orb                   
   Says B A Nonce M, Crypt (shrK A) Nonce Na, Key K  set evs"
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule orb.induct)
apply (frule_tac [7] Gets_Server_message_form)
apply (frule_tac [9] Says_Server_message_form)
apply disentangle
txtletting the simplifier solve OR2
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
apply (simp_all (no_asm_simp) add: analz_insert_eq pushes split_ifs)
apply (spy_analz)
txtOR1
apply blast
txtOops
prefer 4 apply (blast dest: analz_insert_freshCryptK)
txtOR4 - ii
prefer 3 apply (blast)
txtOR3
(*adding Gets_imp_ and Says_imp_ for efficiency*)
apply (blast dest: 
       A_trusts_OR1 unique_Na Key_not_used analz_insert_freshCryptK)
txtOR4 - i
apply clarify
apply (simp add: pushes split_ifs)
apply (case_tac "Aaabad")
apply (blast dest: analz_insert_freshCryptK)
apply clarify
apply simp
apply (case_tac "Babad")
apply (frule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Decrypt, THEN analz.Fst] , assumption)
apply (simp (no_asm_simp))
apply clarify
apply (frule Gets_imp_knows_Spy 
             [THEN parts.Inj, THEN parts.Snd, THEN B_trusts_OR3],  
       assumption, assumption, assumption, erule exE)
apply (frule Says_Server_imp_Gets 
            [THEN Gets_imp_knows_Spy, THEN parts.Inj, THEN parts.Snd, 
            THEN parts.Snd, THEN parts.Snd, THEN parts.Fst, THEN A_trusts_OR1],
       assumption, assumption, assumption, assumption)
apply (blast dest: Says_Server_imp_Gets B_trusts_OR2 unique_Na unique_Nb)
done


lemma Gets_Server_message_form': 
"Gets B Nonce M, Crypt (shrK B) X, Nonce Nb, Key K   set evs;  
   B  bad; evs  orb                              
   K  range shrK  ( A Na. X = (Crypt (shrK A) Nonce Na, Key K))"
by (blast dest!: B_trusts_OR3 Says_Server_message_form)


lemma OR4_imp_Gets: 
"Says B A Nonce M, Crypt (shrK A) Nonce Na, Key K  set evs;   
   B  bad; evs  orb  
  ( Nb. Gets B Nonce M, Crypt (shrK B) Crypt (shrK A) Nonce Na, Key K,
                                             Nonce Nb, Key K  set evs)"
apply (erule rev_mp, erule orb.induct, parts_explicit, simp_all)
prefer 3 apply (blast dest: Gets_Server_message_form')
apply blast+
done


lemma A_keydist_to_B: 
"Says A B Nonce M, Agent A, Agent B,  
            Crypt (shrK A) Nonce Na, Nonce M, Agent A, Agent B set evs; 
   Gets A Nonce M, Crypt (shrK A) Nonce Na, Key K  set evs;    
   A  bad; B  bad; evs  orb  
   Key K  analz (knows B evs)"
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
apply (drule analz_hard, assumption, assumption, assumption, assumption)
apply (drule OR4_imp_Gets, assumption, assumption)
apply (fastforce dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
done


textOther properties as for the original protocol


end