(* Title: HOL/Auth/Kerberos_BAN ID: $Id: Kerberos_BAN.thy,v 1.12 2005/06/17 14:13:06 haftmann Exp $ Author: Giampaolo Bella, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Tidied and converted to Isar by lcp. *) header{*The Kerberos Protocol, BAN Version*} theory Kerberos_BAN imports Public begin text{*From page 251 of Burrows, Abadi and Needham (1989). A Logic of Authentication. Proc. Royal Soc. 426 Confidentiality (secrecy) and authentication properties rely on temporal checks: strong guarantees in a little abstracted - but very realistic - model. *} (* Temporal modelization: session keys can be leaked ONLY when they have expired *) syntax CT :: "event list=>nat" Expired :: "[nat, event list] => bool" RecentAuth :: "[nat, event list] => bool" consts (*Duration of the session key*) SesKeyLife :: nat (*Duration of the authenticator*) AutLife :: nat text{*The ticket should remain fresh for two journeys on the network at least*} specification (SesKeyLife) SesKeyLife_LB [iff]: "2 ≤ SesKeyLife" by blast text{*The authenticator only for one journey*} specification (AutLife) AutLife_LB [iff]: "Suc 0 ≤ AutLife" by blast translations "CT" == "length " "Expired T evs" == "SesKeyLife + T < CT evs" "RecentAuth T evs" == "CT evs ≤ AutLife + T" consts kerberos_ban :: "event list set" inductive "kerberos_ban" intros Nil: "[] ∈ kerberos_ban" Fake: "[| evsf ∈ kerberos_ban; X ∈ synth (analz (spies evsf)) |] ==> Says Spy B X # evsf ∈ kerberos_ban" Kb1: "[| evs1 ∈ kerberos_ban |] ==> Says A Server {|Agent A, Agent B|} # evs1 ∈ kerberos_ban" Kb2: "[| evs2 ∈ kerberos_ban; Key KAB ∉ used evs2; KAB ∈ symKeys; Says A' Server {|Agent A, Agent B|} ∈ set evs2 |] ==> Says Server A (Crypt (shrK A) {|Number (CT evs2), Agent B, Key KAB, (Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) # evs2 ∈ kerberos_ban" Kb3: "[| evs3 ∈ kerberos_ban; Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs3; Says A Server {|Agent A, Agent B|} ∈ set evs3; ~ Expired Ts evs3 |] ==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} # evs3 ∈ kerberos_ban" Kb4: "[| evs4 ∈ kerberos_ban; Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), (Crypt K {|Agent A, Number Ta|}) |}: set evs4; ~ Expired Ts evs4; RecentAuth Ta evs4 |] ==> Says B A (Crypt K (Number Ta)) # evs4 ∈ kerberos_ban" (*Old session keys may become compromised*) Oops: "[| evso ∈ kerberos_ban; Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evso; Expired Ts evso |] ==> Notes Spy {|Number Ts, Key K|} # evso ∈ kerberos_ban" declare Says_imp_knows_Spy [THEN parts.Inj, 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 "[|Key K ∉ used []; K ∈ symKeys|] ==> ∃Timestamp. ∃evs ∈ kerberos_ban. Says B A (Crypt K (Number Timestamp)) ∈ set evs" apply (cut_tac SesKeyLife_LB) apply (intro exI bexI) apply (rule_tac [2] kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4]) apply (possibility, simp_all (no_asm_simp) add: used_Cons) done (**** Inductive proofs about kerberos_ban ****) text{*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*} lemma Kb3_msg_in_parts_spies: "Says S A (Crypt KA {|Timestamp, B, K, X|}) ∈ set evs ==> X ∈ parts (spies evs)" by blast lemma Oops_parts_spies: "Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) ∈ set evs ==> K ∈ parts (spies evs)" by blast text{*Spy never sees another agent's shared key! (unless it's bad at start)*} lemma Spy_see_shrK [simp]: "evs ∈ kerberos_ban ==> (Key (shrK A) ∈ parts (spies evs)) = (A ∈ bad)" apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast+) done lemma Spy_analz_shrK [simp]: "evs ∈ kerberos_ban ==> (Key (shrK A) ∈ analz (spies evs)) = (A ∈ bad)" by auto lemma Spy_see_shrK_D [dest!]: "[| Key (shrK A) ∈ parts (spies evs); evs ∈ kerberos_ban |] ==> A:bad" by (blast dest: Spy_see_shrK) lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] text{*Nobody can have used non-existent keys!*} lemma new_keys_not_used [simp]: "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ kerberos_ban|] ==> K ∉ keysFor (parts (spies evs))" apply (erule rev_mp) apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) txt{*Fake*} apply (force dest!: keysFor_parts_insert) txt{*Kb2, Kb3, Kb4*} apply (force dest!: analz_shrK_Decrypt)+ done subsection{* Lemmas concerning the form of items passed in messages *} text{*Describes the form of K, X and K' when the Server sends this message.*} lemma Says_Server_message_form: "[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) ∈ set evs; evs ∈ kerberos_ban |] ==> K ∉ range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & K' = shrK A" apply (erule rev_mp) apply (erule kerberos_ban.induct, auto) done text{*If the encrypted message appears then it originated with the Server PROVIDED that A is NOT compromised! This shows implicitly the FRESHNESS OF THE SESSION KEY to A *} lemma A_trusts_K_by_Kb2: "[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} ∈ parts (spies evs); A ∉ bad; evs ∈ kerberos_ban |] ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs" apply (erule rev_mp) apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast) done text{*If the TICKET appears then it originated with the Server*} text{*FRESHNESS OF THE SESSION KEY to B*} lemma B_trusts_K_by_Kb3: "[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} ∈ parts (spies evs); B ∉ bad; evs ∈ kerberos_ban |] ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) ∈ set evs" apply (erule rev_mp) apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast) done text{*EITHER describes the form of X when the following message is sent, OR reduces it to the Fake case. Use @{text Says_Server_message_form} if applicable.*} lemma Says_S_message_form: "[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs; evs ∈ kerberos_ban |] ==> (K ∉ range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|})) | X ∈ analz (spies evs)" apply (case_tac "A ∈ bad") apply (force dest!: Says_imp_spies [THEN analz.Inj]) apply (frule Says_imp_spies [THEN parts.Inj]) apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form) done (**** The following is 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. ****) text{* Session keys are not used to encrypt other session keys *} lemma analz_image_freshK [rule_format (no_asm)]: "evs ∈ kerberos_ban ==> ∀K KK. KK ⊆ - (range shrK) --> (Key K ∈ analz (Key`KK Un (spies evs))) = (K ∈ KK | Key K ∈ analz (spies evs))" apply (erule kerberos_ban.induct) apply (drule_tac [7] Says_Server_message_form) apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) done lemma analz_insert_freshK: "[| evs ∈ kerberos_ban; 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) text{* The session key K uniquely identifies the message *} lemma unique_session_keys: "[| Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs; Says Server A' (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) ∈ set evs; evs ∈ kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'" apply (erule rev_mp) apply (erule rev_mp) apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) txt{*Kb2: it can't be a new key*} apply blast done text{* Lemma: the session key sent in msg Kb2 would be EXPIRED if the spy could see it! *} lemma lemma2 [rule_format (no_asm)]: "[| A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) ∈ set evs --> Key K ∈ analz (spies evs) --> Expired Ts evs" apply (erule kerberos_ban.induct) apply (frule_tac [7] Says_Server_message_form) apply (frule_tac [5] Says_S_message_form [THEN disjE]) apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) txt{*Fake*} apply spy_analz txt{*Kb2*} apply (blast intro: parts_insertI less_SucI) txt{*Kb3*} apply (case_tac "Aa ∈ bad") prefer 2 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys) apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) txt{*Oops: PROOF FAILED if addIs below*} apply (blast dest: unique_session_keys intro!: less_SucI) done text{*Confidentiality for the Server: Spy does not see the keys sent in msg Kb2 as long as they have not expired.*} lemma Confidentiality_S: "[| Says Server A (Crypt K' {|Number T, Agent B, Key K, X|}) ∈ set evs; ~ Expired T evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (spies evs)" apply (frule Says_Server_message_form, assumption) apply (blast intro: lemma2) done (**** THE COUNTERPART OF CONFIDENTIALITY [|...; Expired Ts evs; ...|] ==> Key K ∈ analz (spies evs) WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) text{*Confidentiality for Alice*} lemma Confidentiality_A: "[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} ∈ parts (spies evs); ~ Expired T evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (spies evs)" by (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S) text{*Confidentiality for Bob*} lemma Confidentiality_B: "[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} ∈ parts (spies evs); ~ Expired Tk evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (spies evs)" by (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S) lemma lemma_B [rule_format]: "[| B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (spies evs) --> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs --> Crypt K (Number Ta) ∈ parts (spies evs) --> Says B A (Crypt K (Number Ta)) ∈ set evs" apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Says_S_message_form) apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) apply (simp_all (no_asm_simp) add: all_conj_distrib) txt{*Fake*} apply blast txt{*Kb2*} apply (force dest: Crypt_imp_invKey_keysFor) txt{*Kb4*} apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad) done text{*Authentication of B to A*} lemma Authentication_B: "[| Crypt K (Number Ta) ∈ parts (spies evs); Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} ∈ parts (spies evs); ~ Expired Ts evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Says B A (Crypt K (Number Ta)) ∈ set evs" by (blast dest!: A_trusts_K_by_Kb2 intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) lemma lemma_A [rule_format]: "[| A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (spies evs) --> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs --> Crypt K {|Agent A, Number Ta|} ∈ parts (spies evs) --> Says A B {|X, Crypt K {|Agent A, Number Ta|}|} ∈ set evs" apply (erule kerberos_ban.induct) apply (frule_tac [7] Oops_parts_spies) apply (frule_tac [5] Says_S_message_form) apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) apply (simp_all (no_asm_simp) add: all_conj_distrib) txt{*Fake*} apply blast txt{*Kb2*} apply (force dest: Crypt_imp_invKey_keysFor) txt{*Kb3*} apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys) done text{*Authentication of A to B*} lemma Authentication_A: "[| Crypt K {|Agent A, Number Ta|} ∈ parts (spies evs); Crypt (shrK B) {|Number Ts, Agent A, Key K|} ∈ parts (spies evs); ~ Expired Ts evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, Crypt K {|Agent A, Number Ta|}|} ∈ set evs" by (blast dest!: B_trusts_K_by_Kb3 intro!: lemma_A elim!: Confidentiality_S [THEN [2] rev_notE]) end
lemma
[| Key K ∉ used []; K ∈ symKeys |] ==> ∃Timestamp. ∃evs∈kerberos_ban. Says B A (Crypt K (Number Timestamp)) ∈ set evs
lemma Kb3_msg_in_parts_spies:
Says S A (Crypt KA {|Timestamp, B, K, X|}) ∈ set evs ==> X ∈ parts (knows Spy evs)
lemma Oops_parts_spies:
Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) ∈ set evs ==> K ∈ parts (knows Spy evs)
lemma Spy_see_shrK:
evs ∈ kerberos_ban ==> (Key (shrK A) ∈ parts (knows Spy evs)) = (A ∈ bad)
lemma Spy_analz_shrK:
evs ∈ kerberos_ban ==> (Key (shrK A) ∈ analz (knows Spy evs)) = (A ∈ bad)
lemma Spy_see_shrK_D:
[| Key (shrK A) ∈ parts (knows Spy evs); evs ∈ kerberos_ban |] ==> A ∈ bad
lemmas Spy_analz_shrK_D:
[| Key (shrK A) ∈ analz (knows Spy evs); evs ∈ kerberos_ban |] ==> A ∈ bad
lemmas Spy_analz_shrK_D:
[| Key (shrK A) ∈ analz (knows Spy evs); evs ∈ kerberos_ban |] ==> A ∈ bad
lemma new_keys_not_used:
[| Key K ∉ used evs; K ∈ symKeys; evs ∈ kerberos_ban |] ==> K ∉ keysFor (parts (knows Spy evs))
lemma Says_Server_message_form:
[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) ∈ set evs; evs ∈ kerberos_ban |] ==> K ∉ range shrK ∧ X = Crypt (shrK B) {|Number Ts, Agent A, Key K|} ∧ K' = shrK A
lemma A_trusts_K_by_Kb2:
[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} ∈ parts (knows Spy evs); A ∉ bad; evs ∈ kerberos_ban |] ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs
lemma B_trusts_K_by_Kb3:
[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} ∈ parts (knows Spy evs); B ∉ bad; evs ∈ kerberos_ban |] ==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) ∈ set evs
lemma Says_S_message_form:
[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs; evs ∈ kerberos_ban |] ==> K ∉ range shrK ∧ X = Crypt (shrK B) {|Number Ts, Agent A, Key K|} ∨ X ∈ analz (knows Spy evs)
lemma analz_image_freshK:
[| evs ∈ kerberos_ban; KK ⊆ - range shrK |] ==> (Key K ∈ analz (Key ` KK ∪ knows Spy evs)) = (K ∈ KK ∨ Key K ∈ analz (knows Spy evs))
lemma analz_insert_freshK:
[| evs ∈ kerberos_ban; KAB ∉ range shrK |] ==> (Key K ∈ analz (insert (Key KAB) (knows Spy evs))) = (K = KAB ∨ Key K ∈ analz (knows Spy evs))
lemma unique_session_keys:
[| Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs; Says Server A' (Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) ∈ set evs; evs ∈ kerberos_ban |] ==> A = A' ∧ Ts = Ts' ∧ B = B' ∧ X = X'
lemma lemma2:
[| A ∉ bad; B ∉ bad; evs ∈ kerberos_ban; Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) ∈ set evs; Key K ∈ analz (knows Spy evs) |] ==> Expired Ts evs
lemma Confidentiality_S:
[| Says Server A (Crypt K' {|Number T, Agent B, Key K, X|}) ∈ set evs; ¬ Expired T evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (knows Spy evs)
lemma Confidentiality_A:
[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} ∈ parts (knows Spy evs); ¬ Expired T evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (knows Spy evs)
lemma Confidentiality_B:
[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} ∈ parts (knows Spy evs); ¬ Expired Tk evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Key K ∉ analz (knows Spy evs)
lemma lemma_B:
[| B ∉ bad; evs ∈ kerberos_ban; Key K ∉ analz (knows Spy evs); Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs; Crypt K (Number Ta) ∈ parts (knows Spy evs) |] ==> Says B A (Crypt K (Number Ta)) ∈ set evs
lemma Authentication_B:
[| Crypt K (Number Ta) ∈ parts (knows Spy evs); Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} ∈ parts (knows Spy evs); ¬ Expired Ts evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Says B A (Crypt K (Number Ta)) ∈ set evs
lemma lemma_A:
[| A ∉ bad; B ∉ bad; evs ∈ kerberos_ban; Key K ∉ analz (knows Spy evs); Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) ∈ set evs; Crypt K {|Agent A, Number Ta|} ∈ parts (knows Spy evs) |] ==> Says A B {|X, Crypt K {|Agent A, Number Ta|}|} ∈ set evs
lemma Authentication_A:
[| Crypt K {|Agent A, Number Ta|} ∈ parts (knows Spy evs); Crypt (shrK B) {|Number Ts, Agent A, Key K|} ∈ parts (knows Spy evs); ¬ Expired Ts evs; A ∉ bad; B ∉ bad; evs ∈ kerberos_ban |] ==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, Crypt K {|Agent A, Number Ta|}|} ∈ set evs