Quelle  Public.thy   Sprache: Isabelle

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

Theory of Public Keys (common to all public-key protocols)

Private and public keys; initial states of agents
*)

theory Public
imports Event
begin

lemma invKey_K: "K \ symKeys \ invKey K = K"
by (simp add: symKeys_def)

subsection‹Asymmetric Keys›

datatype keymode = Signature | Encryption

consts
  publicKey :: "[keymode,agent] \ key"

abbreviation
  pubEK :: "agent \ key" where
  "pubEK == publicKey Encryption"

abbreviation
  pubSK :: "agent \ key" where
  "pubSK == publicKey Signature"

abbreviation
  privateKey :: "[keymode, agent] \ key" where
  "privateKey b A == invKey (publicKey b A)"

abbreviation
  (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
  priEK :: "agent \ key" where
  "priEK A == privateKey Encryption A"

abbreviation
  priSK :: "agent \ key" where
  "priSK A == privateKey Signature A"


text‹These abbreviations give backward compatibility.  They represent the
simple situation where the signature and encryption keys are the same.›

abbreviation (input)
  pubK :: "agent \ key" where
  "pubK A == pubEK A"

abbreviation (input)
  priK :: "agent \ key" where
  "priK A == invKey (pubEK A)"


text‹By freeness of agents, no two agents have the same key.  Since
  🍋‹True≠False›, no agent has identical signing and encryption keys›
specification (publicKey)
  injective_publicKey:
    "publicKey b A = publicKey c A' \ b=c \ A=A'"
   apply (rule exI [of _ 
       "\b A. 2 * case_agent 0 (\n. n + 2) 1 A + case_keymode 0 1 b"])
   apply (auto simp add: inj_on_def split: agent.split keymode.split)
   apply presburger
   apply presburger
   done                       


axiomatization where
  (*No private key equals any public key (essential to ensure that private
    keys are private!) *)
  privateKey_neq_publicKey [iff]: "privateKey b A \ publicKey c A'"

lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym]
declare publicKey_neq_privateKey [iff]


subsection‹Basic properties of 🍋‹pubK› and 🍋‹priK››

lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c \ A=A')"
by (blast dest!: injective_publicKey) 

lemma not_symKeys_pubK [iff]: "publicKey b A \ symKeys"
by (simp add: symKeys_def)

lemma not_symKeys_priK [iff]: "privateKey b A \ symKeys"
by (simp add: symKeys_def)

lemma symKey_neq_priEK: "K \ symKeys \ K \ priEK A"
by auto

lemma symKeys_neq_imp_neq: "(K \ symKeys) \ (K' \ symKeys) \ K \ K'"
by blast

lemma symKeys_invKey_iff [iff]: "(invKey K \ symKeys) = (K \ symKeys)"
  unfolding symKeys_def by auto

lemma analz_symKeys_Decrypt:
     "\Crypt K X \ analz H; K \ symKeys; Key K \ analz H\
      ==> X ∈ analz H"
by (auto simp add: symKeys_def)



subsection‹"Image" equations that hold for injective functions›

lemma invKey_image_eq [simp]: "(invKey x \ invKey`A) = (x \ A)"
by auto

(*holds because invKey is injective*)
lemma publicKey_image_eq [simp]:
     "(publicKey b x \ publicKey c ` AA) = (b=c \ x \ AA)"
by auto

lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \ publicKey c ` AA"
by auto

lemma privateKey_image_eq [simp]:
     "(privateKey b A \ invKey ` publicKey c ` AS) = (b=c \ A\AS)"
by auto

lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \ invKey ` publicKey c ` AS"
by auto


subsection‹Symmetric Keys›

text‹For some protocols, it is convenient to equip agents with symmetric as
well as asymmetric keys.  The theory ‹Shared› assumes that all keys
are symmetric.›

consts
  shrK    :: "agent => key"    🍋 ‹long-term shared keys›

specification (shrK)
  inj_shrK: "inj shrK"
  🍋 ‹No two agents have the same long-term key›
   apply (rule exI [of _ "case_agent 0 (\n. n + 2) 1"]) 
   apply (simp add: inj_on_def split: agent.split) 
   done

axiomatization where
  sym_shrK [iff]: "shrK X \ symKeys" 🍋 ‹All shared keys are symmetric›

text‹Injectiveness: Agents' long-term keys are distinct.\
lemmas shrK_injective = inj_shrK [THEN inj_eq]
declare shrK_injective [iff]

lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A"
by (simp add: invKey_K) 

lemma analz_shrK_Decrypt:
     "\Crypt (shrK A) X \ analz H; Key(shrK A) \ analz H\ \ X \ analz H"
by auto

lemma analz_Decrypt':
     "\Crypt K X \ analz H; K \ symKeys; Key K \ analz H\ \ X \ analz H"
by (auto simp add: invKey_K)

lemma priK_neq_shrK [iff]: "shrK A \ privateKey b C"
by (simp add: symKeys_neq_imp_neq)

lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym]
declare shrK_neq_priK [simp]

lemma pubK_neq_shrK [iff]: "shrK A \ publicKey b C"
by (simp add: symKeys_neq_imp_neq)

lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym]
declare shrK_neq_pubK [simp]

lemma priEK_noteq_shrK [simp]: "priEK A \ shrK B" 
by auto

lemma publicKey_notin_image_shrK [simp]: "publicKey b x \ shrK ` AA"
by auto

lemma privateKey_notin_image_shrK [simp]: "privateKey b x \ shrK ` AA"
by auto

lemma shrK_notin_image_publicKey [simp]: "shrK x \ publicKey b ` AA"
by auto

lemma shrK_notin_image_privateKey [simp]: "shrK x \ invKey ` publicKey b ` AA" 
by auto

lemma shrK_image_eq [simp]: "(shrK x \ shrK ` AA) = (x \ AA)"
by auto

text‹For some reason, moving this up can make some proofs loop!›
declare invKey_K [simp]


subsection‹Initial States of Agents›

text‹Note: for all practical purposes, all that matters is the initial
knowledge of the Spy.  All other agents are automata, merely following the
protocol.›

overloading
  initState ≡ initState
begin

primrec initState where
        (*Agents know their private key and all public keys*)
  initState_Server:
    "initState Server =
       {Key (priEK Server), Key (priSK Server)} ∪ 
       (Key ` range pubEK) ∪ (Key ` range pubSK) ∪ (Key ` range shrK)"

| initState_Friend:
    "initState (Friend i) =
       {Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} ∪ 
       (Key ` range pubEK) ∪ (Key ` range pubSK)"

| initState_Spy:
    "initState Spy =
       (Key ` invKey ` pubEK ` bad) ∪ (Key ` invKey ` pubSK ` bad) ∪ 
       (Key ` shrK ` bad) ∪ 
       (Key ` range pubEK) ∪ (Key ` range pubSK)"

end


text‹These lemmas allow reasoning about 🍋‹used evs› rather than
   🍋‹knows Spy evs›, which is useful when there are private Notes. 
   Because they depend upon the definition of 🍋‹initState›, they cannot
   be moved up.›

lemma used_parts_subset_parts [rule_format]:
     "\X \ used evs. parts {X} \ used evs"
apply (induct evs) 
 prefer 2
 apply (simp add: used_Cons split: event.split)
 apply (metis Un_iff empty_subsetI insert_subset le_supI1 le_supI2 parts_subset_iff)
txt‹Base case›
apply (auto dest!: parts_cut simp add: used_Nil) 
done

lemma MPair_used_D: "\X,Y\ \ used H \ X \ used H \ Y \ used H"
by (drule used_parts_subset_parts, simp, blast)

text‹There was a similar theorem in Event.thy, so perhaps this one can
  be moved up if proved directly by induction.›
lemma MPair_used [elim!]:
     "\\X,Y\ \ used H;
         [X ∈ used H; Y ∈ used H] ==> P] 
      ==> P"
by (blast dest: MPair_used_D) 


text‹Rewrites should not refer to  🍋‹initState(Friend i)› because
  that expression is not in normal form.›

lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
unfolding keysFor_def
apply (induct_tac "C")
apply (auto intro: range_eqI)
done

lemma Crypt_notin_initState: "Crypt K X \ parts (initState B)"
by (induct B, auto)

lemma Crypt_notin_used_empty [simp]: "Crypt K X \ used []"
by (simp add: Crypt_notin_initState used_Nil)

(*** Basic properties of shrK ***)

(*Agents see their own shared keys!*)
lemma shrK_in_initState [iff]: "Key (shrK A) \ initState A"
by (induct_tac "A", auto)

lemma shrK_in_knows [iff]: "Key (shrK A) \ knows A evs"
by (simp add: initState_subset_knows [THEN subsetD])

lemma shrK_in_used [iff]: "Key (shrK A) \ used evs"
by (rule initState_into_used, blast)


(** Fresh keys never clash with long-term shared keys **)

(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
  from long-term shared keys*)
lemma Key_not_used [simp]: "Key K \ used evs \ K \ range shrK"
by blast

lemma shrK_neq: "Key K \ used evs \ shrK B \ K"
by blast

lemmas neq_shrK = shrK_neq [THEN not_sym]
declare neq_shrK [simp]


subsection‹Function 🍋‹spies››

lemma not_SignatureE [elim!]: "b \ Signature \ b = Encryption"
  by (cases b, auto) 

text‹Agents see their own private keys!›
lemma priK_in_initState [iff]: "Key (privateKey b A) \ initState A"
  by (cases A, auto)

text‹Agents see all public keys!›
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \ initState B"
  by (cases B, auto) 

text‹All public keys are visible›
lemma spies_pubK [iff]: "Key (publicKey b A) \ spies evs"
apply (induct_tac "evs")
apply (auto simp add: imageI knows_Cons split: event.split)
done

lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj]
declare analz_spies_pubK [iff]

text‹Spy sees private keys of bad agents!›
lemma Spy_spies_bad_privateKey [intro!]:
     "A \ bad \ Key (privateKey b A) \ spies evs"
apply (induct_tac "evs")
apply (auto simp add: imageI knows_Cons split: event.split)
done

text‹Spy sees long-term shared keys of bad agents!›
lemma Spy_spies_bad_shrK [intro!]:
     "A \ bad \ Key (shrK A) \ spies evs"
apply (induct_tac "evs")
apply (simp_all add: imageI knows_Cons split: event.split)
done

lemma publicKey_into_used [iff] :"Key (publicKey b A) \ used evs"
apply (rule initState_into_used)
apply (rule publicKey_in_initState [THEN parts.Inj])
done

lemma privateKey_into_used [iff]: "Key (privateKey b A) \ used evs"
apply(rule initState_into_used)
apply(rule priK_in_initState [THEN parts.Inj])
done

(*For case analysis on whether or not an agent is compromised*)
lemma Crypt_Spy_analz_bad:
     "\Crypt (shrK A) X \ analz (knows Spy evs); A \ bad\
      ==> X ∈ analz (knows Spy evs)"
by force


subsection‹Fresh Nonces›

lemma Nonce_notin_initState [iff]: "Nonce N \ parts (initState B)"
by (induct_tac "B", auto)

lemma Nonce_notin_used_empty [simp]: "Nonce N \ used []"
by (simp add: used_Nil)


subsection‹Supply fresh nonces for possibility theorems›

text‹In any trace, there is an upper bound N on the greatest nonce in use›
lemma Nonce_supply_lemma: "\N. \n. N\n \ Nonce n \ used evs"
apply (induct_tac "evs")
apply (rule_tac x = 0 in exI)
apply (simp_all (no_asm_simp) add: used_Cons split: event.split)
apply safe
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+
done

lemma Nonce_supply1: "\N. Nonce N \ used evs"
by (rule Nonce_supply_lemma [THEN exE], blast)

lemma Nonce_supply: "Nonce (SOME N. Nonce N \ used evs) \ used evs"
apply (rule Nonce_supply_lemma [THEN exE])
apply (rule someI, fast)
done

subsection‹Specialized Rewriting for Theorems About 🍋‹analz› and Image›

lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \ H"
by blast

lemma insert_Key_image: "insert (Key K) (Key`KK \ C) = Key ` (insert K KK) \ C"
by blast


lemma Crypt_imp_keysFor :"\Crypt K X \ H; K \ symKeys\ \ K \ keysFor H"
by (drule Crypt_imp_invKey_keysFor, simp)

text‹Lemma for the trivial direction of the if-and-only-if of the 
Session Key Compromise Theorem›
lemma analz_image_freshK_lemma:
     "(Key K \ analz (Key`nE \ H)) \ (K \ nE | Key K \ analz H) \
         (Key K ∈ analz (Key`nE ∪ H)) = (K ∈ nE | Key K ∈ analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])

lemmas analz_image_freshK_simps =
       simp_thms mem_simps 🍋 ‹these two allow its use with ‹only:››
       disj_comms 
       image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset
       analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]
       insert_Key_singleton 
       Key_not_used insert_Key_image Un_assoc [THEN sym]

ML ‹
structure Public =
struct

val analz_image_freshK_ss =
  simpset_of
   (🍋 |> Simplifier.del_simps @{thms image_insert image_Un}
    |> Simplifier.del_simps @{thms imp_disjL}    (*reduces blow-up*)
    |> Simplifier.add_simps @{thms analz_image_freshK_simps})

(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
    REPEAT (*omit used_Says so that Nonces start from different traces!*)
    (ALLGOALS (simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver |> Simplifier.del_simp @{thm used_Says}))
     THEN
     REPEAT_FIRST (eq_assume_tac ORELSE'
                   resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))

(*For harder protocols (such as Recur) where we have to set up some
  nonces and keys initially*)
fun basic_possibility_tac ctxt =
    REPEAT 
    (ALLGOALS (asm_simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver))
     THEN
     REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))

end
›

method_setup analz_freshK = ‹
    Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD
      (EVERY [REPEAT_FIRST (resolve_tac ctxt @{thms allI ballI impI}),
          REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}),
          ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))])))›
    "for proving the Session Key Compromise theorem"


subsection‹Specialized Methods for Possibility Theorems›

method_setup possibility = ‹
    Scan.succeed (SIMPLE_METHOD o Public.possibility_tac)›
    "for proving possibility theorems"

method_setup basic_possibility = ‹
    Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac)›
    "for proving possibility theorems"

end