Theory TLS

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

Inductive relation "tls" for the TLS (Transport Layer Security) protocol.
This protocol is essentially the same as SSL 3.0.

Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
Allen, Transport Layer Security Working Group, 21 May 1997,
INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
to that memo.

An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
global signing authority.

A is the client and B is the server, not to be confused with the constant
Server, who is in charge of all public keys.

The model assumes that no fraudulent certificates are present, but it does
assume that some private keys are to the spy.

REMARK.  The event "Notes A ⦃Agent B, Nonce PMS⦄" appears in ClientKeyExch,
CertVerify, ClientFinished to record that A knows M.  It is a note from A to
herself.  Nobody else can see it.  In ClientKeyExch, the Spy can substitute
his own certificate for A's, but he cannot replace A's note by one for himself.

The Note event avoids a weakness in the public-key model.  Each
agent's state is recorded as the trace of messages.  When the true client (A)
invents PMS, he encrypts PMS with B's public key before sending it.  The model
does not distinguish the original occurrence of such a message from a replay.
In the shared-key model, the ability to encrypt implies the ability to
decrypt, so the problem does not arise.

Proofs would be simpler if ClientKeyExch included A's name within
Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
about that message (which B receives) and the stronger event
Notes A ⦃Agent B, Nonce PMS⦄.
*)

sectionThe TLS Protocol: Transport Layer Security

theory TLS imports Public "HOL-Library.Nat_Bijection" begin

definition certificate :: "[agent,key]  msg" where
    "certificate A KA == Crypt (priSK Server) Agent A, Key KA"

textTLS apparently does not require separate keypairs for encryption and
signature.  Therefore, we formalize signature as encryption using the
private encryption key.

datatype role = ClientRole | ServerRole

consts
  (*Pseudo-random function of Section 5*)
  PRF  :: "nat*nat*nat  nat"

  (*Client, server write keys are generated uniformly by function sessionK
    to avoid duplicating their properties.  They are distinguished by a
    tag (not a bool, to avoid the peculiarities of if-and-only-if).
    Session keys implicitly include MAC secrets.*)
  sessionK :: "(nat*nat*nat) * role  key"

abbreviation
  clientK :: "nat*nat*nat  key" where
  "clientK X == sessionK(X, ClientRole)"

abbreviation
  serverK :: "nat*nat*nat  key" where
  "serverK X == sessionK(X, ServerRole)"


specification (PRF)
  inj_PRF: "inj PRF"
  ― ‹the pseudo-random function is collision-free
   apply (rule exI [of _ "λ(x,y,z). prod_encode(x, prod_encode(y,z))"])
   apply (simp add: inj_on_def prod_encode_eq)
   done

specification (sessionK)
  inj_sessionK: "inj sessionK"
  ― ‹sessionK is collision-free; also, no clientK clashes with any serverK.
   apply (rule exI [of _ 
         "λ((x,y,z), r). prod_encode(case_role 0 1 r, 
                           prod_encode(x, prod_encode(y,z)))"])
   apply (simp add: inj_on_def prod_encode_eq split: role.split) 
   done

axiomatization where
  ― ‹sessionK makes symmetric keys
  isSym_sessionK: "sessionK nonces  symKeys" and

  ― ‹sessionK never clashes with a long-term symmetric key  
     (they don't exist in TLS anyway)
  sessionK_neq_shrK [iff]: "sessionK nonces  shrK A"


inductive_set tls :: "event list set"
  where
   Nil:  ― ‹The initial, empty trace
         "[]  tls"

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

 | SpyKeys: ― ‹The spy may apply termPRF and termsessionK
                to available nonces
         "[| evsSK  tls;
             {Nonce NA, Nonce NB, Nonce M}  analz (spies evsSK) |]
          ==> Notes Spy  Nonce (PRF(M,NA,NB)),
                           Key (sessionK((NA,NB,M),role)) # evsSK  tls"

 | ClientHello:
         ― ‹(7.4.1.2)
           PA represents CLIENT_VERSION›, CIPHER_SUITES› and COMPRESSION_METHODS›.
           It is uninterpreted but will be confirmed in the FINISHED messages.
           NA is CLIENT RANDOM, while SID is SESSION_ID›.
           UNIX TIME is omitted because the protocol doesn't use it.
           May assume termNA  range PRF because CLIENT RANDOM is 
           28 bytes while MASTER SECRET is 48 bytes
         "[| evsCH  tls;  Nonce NA  used evsCH;  NA  range PRF |]
          ==> Says A B Agent A, Nonce NA, Number SID, Number PA
                # evsCH    tls"

 | ServerHello:
         ― ‹7.4.1.3 of the TLS Internet-Draft
           PB represents CLIENT_VERSION›, CIPHER_SUITE› and COMPRESSION_METHOD›.
           SERVER CERTIFICATE (7.4.2) is always present.
           CERTIFICATE_REQUEST› (7.4.4) is implied.
         "[| evsSH  tls;  Nonce NB  used evsSH;  NB  range PRF;
             Says A' B Agent A, Nonce NA, Number SID, Number PA
                set evsSH |]
          ==> Says B A Nonce NB, Number SID, Number PB # evsSH    tls"

 | Certificate:
         ― ‹SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.
         "evsC  tls ==> Says B A (certificate B (pubK B)) # evsC    tls"

 | ClientKeyExch:
         ― ‹CLIENT KEY EXCHANGE (7.4.7).
           The client, A, chooses PMS, the PREMASTER SECRET.
           She encrypts PMS using the supplied KB, which ought to be pubK B.
           We assume termPMS  range PRF because a clash betweem the PMS
           and another MASTER SECRET is highly unlikely (even though
           both items have the same length, 48 bytes).
           The Note event records in the trace that she knows PMS
               (see REMARK at top).
         "[| evsCX  tls;  Nonce PMS  used evsCX;  PMS  range PRF;
             Says B' A (certificate B KB)  set evsCX |]
          ==> Says A B (Crypt KB (Nonce PMS))
              # Notes A Agent B, Nonce PMS
              # evsCX    tls"

 | CertVerify:
        ― ‹The optional Certificate Verify (7.4.8) message contains the
          specific components listed in the security analysis, F.1.1.2.
          It adds the pre-master-secret, which is also essential!
          Checking the signature, which is the only use of A's certificate,
          assures B of A's presence
         "[| evsCV  tls;
             Says B' A Nonce NB, Number SID, Number PB  set evsCV;
             Notes A Agent B, Nonce PMS  set evsCV |]
          ==> Says A B (Crypt (priK A) (HashNonce NB, Agent B, Nonce PMS))
              # evsCV    tls"

        ― ‹Finally come the FINISHED messages (7.4.8), confirming PA and PB
          among other things.  The master-secret is PRF(PMS,NA,NB).
          Either party may send its message first.

 | ClientFinished:
        ― ‹The occurrence of Notes A ⦃Agent B, Nonce PMS⦄› stops the
          rule's applying when the Spy has satisfied the Says A B› by
          repaying messages sent by the true client; in that case, the
          Spy does not know PMS and could not send ClientFinished.  One
          could simply put termASpy into the rule, but one should not
          expect the spy to be well-behaved.
         "[| evsCF  tls;
             Says A  B Agent A, Nonce NA, Number SID, Number PA
                set evsCF;
             Says B' A Nonce NB, Number SID, Number PB  set evsCF;
             Notes A Agent B, Nonce PMS  set evsCF;
             M = PRF(PMS,NA,NB) |]
          ==> Says A B (Crypt (clientK(NA,NB,M))
                        (HashNumber SID, Nonce M,
                               Nonce NA, Number PA, Agent A,
                               Nonce NB, Number PB, Agent B))
              # evsCF    tls"

 | ServerFinished:
        ― ‹Keeping A' and A'' distinct means B cannot even check that the
          two messages originate from the same source.
         "[| evsSF  tls;
             Says A' B  Agent A, Nonce NA, Number SID, Number PA
                set evsSF;
             Says B  A  Nonce NB, Number SID, Number PB  set evsSF;
             Says A'' B (Crypt (pubK B) (Nonce PMS))  set evsSF;
             M = PRF(PMS,NA,NB) |]
          ==> Says B A (Crypt (serverK(NA,NB,M))
                        (HashNumber SID, Nonce M,
                               Nonce NA, Number PA, Agent A,
                               Nonce NB, Number PB, Agent B))
              # evsSF    tls"

 | ClientAccepts:
        ― ‹Having transmitted ClientFinished and received an identical
          message encrypted with serverK, the client stores the parameters
          needed to resume this session.  The "Notes A ..." premise is
          used to prove Notes_master_imp_Crypt_PMS›.
         "[| evsCA  tls;
             Notes A Agent B, Nonce PMS  set evsCA;
             M = PRF(PMS,NA,NB);
             X = HashNumber SID, Nonce M,
                       Nonce NA, Number PA, Agent A,
                       Nonce NB, Number PB, Agent B;
             Says A  B (Crypt (clientK(NA,NB,M)) X)  set evsCA;
             Says B' A (Crypt (serverK(NA,NB,M)) X)  set evsCA |]
          ==>
             Notes A Number SID, Agent A, Agent B, Nonce M # evsCA    tls"

 | ServerAccepts:
        ― ‹Having transmitted ServerFinished and received an identical
          message encrypted with clientK, the server stores the parameters
          needed to resume this session.  The "Says A'' B ..." premise is
          used to prove Notes_master_imp_Crypt_PMS›.
         "[| evsSA  tls;
             A  B;
             Says A'' B (Crypt (pubK B) (Nonce PMS))  set evsSA;
             M = PRF(PMS,NA,NB);
             X = HashNumber SID, Nonce M,
                       Nonce NA, Number PA, Agent A,
                       Nonce NB, Number PB, Agent B;
             Says B  A (Crypt (serverK(NA,NB,M)) X)  set evsSA;
             Says A' B (Crypt (clientK(NA,NB,M)) X)  set evsSA |]
          ==>
             Notes B Number SID, Agent A, Agent B, Nonce M # evsSA    tls"

 | ClientResume:
         ― ‹If A recalls the SESSION_ID›, then she sends a FINISHED
             message using the new nonces and stored MASTER SECRET.
         "[| evsCR  tls;
             Says A  B Agent A, Nonce NA, Number SID, Number PA  set evsCR;
             Says B' A Nonce NB, Number SID, Number PB  set evsCR;
             Notes A Number SID, Agent A, Agent B, Nonce M  set evsCR |]
          ==> Says A B (Crypt (clientK(NA,NB,M))
                        (HashNumber SID, Nonce M,
                               Nonce NA, Number PA, Agent A,
                               Nonce NB, Number PB, Agent B))
              # evsCR    tls"

 | ServerResume:
         ― ‹Resumption (7.3):  If B finds the SESSION_ID› then he can 
             send a FINISHED message using the recovered MASTER SECRET
         "[| evsSR  tls;
             Says A' B Agent A, Nonce NA, Number SID, Number PA  set evsSR;
             Says B  A Nonce NB, Number SID, Number PB  set evsSR;
             Notes B Number SID, Agent A, Agent B, Nonce M  set evsSR |]
          ==> Says B A (Crypt (serverK(NA,NB,M))
                        (HashNumber SID, Nonce M,
                               Nonce NA, Number PA, Agent A,
                               Nonce NB, Number PB, Agent B)) # evsSR
                  tls"

 | Oops:
         ― ‹The most plausible compromise is of an old session key.  Losing
           the MASTER SECRET or PREMASTER SECRET is more serious but
           rather unlikely.  The assumption termASpy is essential: 
           otherwise the Spy could learn session keys merely by 
           replaying messages!
         "[| evso  tls;  A  Spy;
             Says A B (Crypt (sessionK((NA,NB,M),role)) X)  set evso |]
          ==> Says A Spy (Key (sessionK((NA,NB,M),role))) # evso    tls"

(*
Protocol goals:
* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
     parties (though A is not necessarily authenticated).

* B upon receiving CertVerify knows that A is present (But this
    message is optional!)

* A upon receiving ServerFinished knows that B is present

* Each party who has received a FINISHED message can trust that the other
  party agrees on all message components, including PA and PB (thus foiling
  rollback attacks).
*)

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]


textAutomatically unfold the definition of "certificate"
declare certificate_def [simp]

textInjectiveness of key-generating functions
declare inj_PRF [THEN inj_eq, iff]
declare inj_sessionK [THEN inj_eq, iff]
declare isSym_sessionK [simp]


(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)

lemma pubK_neq_sessionK [iff]: "publicKey b A  sessionK arg"
by (simp add: symKeys_neq_imp_neq)

declare pubK_neq_sessionK [THEN not_sym, iff]

lemma priK_neq_sessionK [iff]: "invKey (publicKey b A)  sessionK arg"
by (simp add: symKeys_neq_imp_neq)

declare priK_neq_sessionK [THEN not_sym, iff]

lemmas keys_distinct = pubK_neq_sessionK priK_neq_sessionK


subsectionProtocol Proofs

textPossibility properties state that some traces run the protocol to the
end.  Four paths and 12 rules are considered.


(** These proofs assume that the Nonce_supply nonces
        (which have the form  @ N. Nonce N ∉ used evs)
    lie outside the range of PRF.  It seems reasonable, but as it is needed
    only for the possibility theorems, it is not taken as an axiom.
**)


textPossibility property ending with ClientAccepts.
lemma "[| evs. (SOME N. Nonce N  used evs)  range PRF;  A  B |]
      ==> SID M. evs  tls.
            Notes A Number SID, Agent A, Agent B, Nonce M  set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.Nil
                    [THEN tls.ClientHello, THEN tls.ServerHello,
                     THEN tls.Certificate, THEN tls.ClientKeyExch,
                     THEN tls.ClientFinished, THEN tls.ServerFinished,
                     THEN tls.ClientAccepts], possibility, blast+)
done


textAnd one for ServerAccepts.  Either FINISHED message may come first.
lemma "[| evs. (SOME N. Nonce N  used evs)  range PRF; A  B |]
      ==> SID NA PA NB PB M. evs  tls.
           Notes B Number SID, Agent A, Agent B, Nonce M  set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.Nil
                    [THEN tls.ClientHello, THEN tls.ServerHello,
                     THEN tls.Certificate, THEN tls.ClientKeyExch,
                     THEN tls.ServerFinished, THEN tls.ClientFinished, 
                     THEN tls.ServerAccepts], possibility, blast+)
done


textAnother one, for CertVerify (which is optional)
lemma "[| evs. (SOME N. Nonce N  used evs)  range PRF;  A  B |]
       ==> NB PMS. evs  tls.
              Says A B (Crypt (priK A) (HashNonce NB, Agent B, Nonce PMS)) 
                 set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.Nil
                    [THEN tls.ClientHello, THEN tls.ServerHello,
                     THEN tls.Certificate, THEN tls.ClientKeyExch,
                     THEN tls.CertVerify], possibility, blast+)
done


textAnother one, for session resumption (both ServerResume and ClientResume).
  NO tls.Nil here: we refer to a previous session, not the empty trace.
lemma "[| evs0  tls;
          Notes A Number SID, Agent A, Agent B, Nonce M  set evs0;
          Notes B Number SID, Agent A, Agent B, Nonce M  set evs0;
          evs. (SOME N. Nonce N  used evs)  range PRF;
          A  B |]
      ==> NA PA NB PB X. evs  tls.
                X = HashNumber SID, Nonce M,
                          Nonce NA, Number PA, Agent A,
                          Nonce NB, Number PB, Agent B  
                Says A B (Crypt (clientK(NA,NB,M)) X)  set evs  
                Says B A (Crypt (serverK(NA,NB,M)) X)  set evs"
apply (intro exI bexI)
apply (rule_tac [2] tls.ClientHello
                    [THEN tls.ServerHello,
                     THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+)
done


subsectionInductive proofs about tls


(** Theorems of the form X ∉ parts (spies evs) imply that NOBODY
    sends messages containing X! **)

textSpy never sees a good agent's private key!
lemma Spy_see_priK [simp]:
     "evs  tls ==> (Key (privateKey b A)  parts (spies evs)) = (A  bad)"
by (erule tls.induct, force, simp_all, blast)

lemma Spy_analz_priK [simp]:
     "evs  tls ==> (Key (privateKey b A)  analz (spies evs)) = (A  bad)"
by auto

lemma Spy_see_priK_D [dest!]:
    "[|Key (privateKey b A)  parts (knows Spy evs);  evs  tls|] ==> A  bad"
by (blast dest: Spy_see_priK)


textThis lemma says that no false certificates exist.  One might extend the
  model to include bogus certificates for the agents, but there seems
  little point in doing so: the loss of their private keys is a worse
  breach of security.
lemma certificate_valid:
    "[| certificate B KB  parts (spies evs);  evs  tls |] ==> KB = pubK B"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all, blast) 
done

lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]


subsubsectionProperties of items found in Notes

lemma Notes_Crypt_parts_spies:
     "[| Notes A Agent B, X  set evs;  evs  tls |]
      ==> Crypt (pubK B) X  parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, 
       frule_tac [7] CX_KB_is_pubKB, force, simp_all)
apply (blast intro: parts_insertI)
done

textC may be either A or B
lemma Notes_master_imp_Crypt_PMS:
     "[| Notes C s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))  set evs;
         evs  tls |]
      ==> Crypt (pubK B) (Nonce PMS)  parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
txtFake
apply (blast intro: parts_insertI)
txtClient, Server Accept
apply (blast dest!: Notes_Crypt_parts_spies)+
done

textCompared with the theorem above, both premise and conclusion are stronger
lemma Notes_master_imp_Notes_PMS:
     "[| Notes A s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))  set evs;
         evs  tls |]
      ==> Notes A Agent B, Nonce PMS  set evs"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
txtServerAccepts
apply blast
done


subsubsectionProtocol goal: if B receives CertVerify, then A sent it

textB can check A's signature if he has received A's certificate.
lemma TrustCertVerify_lemma:
     "[| X  parts (spies evs);
         X = Crypt (priK A) (Hashnb, Agent B, pms);
         evs  tls;  A  bad |]
      ==> Says A B X  set evs"
apply (erule rev_mp, erule ssubst)
apply (erule tls.induct, force, simp_all, blast)
done

textFinal version: B checks X using the distributed KA instead of priK A
lemma TrustCertVerify:
     "[| X  parts (spies evs);
         X = Crypt (invKey KA) (Hashnb, Agent B, pms);
         certificate A KA  parts (spies evs);
         evs  tls;  A  bad |]
      ==> Says A B X  set evs"
by (blast dest!: certificate_valid intro!: TrustCertVerify_lemma)


textIf CertVerify is present then A has chosen PMS.
lemma UseCertVerify_lemma:
     "[| Crypt (priK A) (Hashnb, Agent B, Nonce PMS)  parts (spies evs);
         evs  tls;  A  bad |]
      ==> Notes A Agent B, Nonce PMS  set evs"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all, blast)
done

textFinal version using the distributed KA instead of priK A
lemma UseCertVerify:
     "[| Crypt (invKey KA) (Hashnb, Agent B, Nonce PMS)
            parts (spies evs);
         certificate A KA  parts (spies evs);
         evs  tls;  A  bad |]
      ==> Notes A Agent B, Nonce PMS  set evs"
by (blast dest!: certificate_valid intro!: UseCertVerify_lemma)


lemma no_Notes_A_PRF [simp]:
     "evs  tls ==> Notes A Agent B, Nonce (PRF x)  set evs"
apply (erule tls.induct, force, simp_all)
txtClientKeyExch: PMS is assumed to differ from any PRF.
apply blast
done


lemma MS_imp_PMS [dest!]:
     "[| Nonce (PRF (PMS,NA,NB))  parts (spies evs);  evs  tls |]
      ==> Nonce PMS  parts (spies evs)"
apply (erule rev_mp)
apply (erule tls.induct, force, simp_all)
txtFake
apply (blast intro: parts_insertI)
txtEasy, e.g. by freshness
apply (blast dest: Notes_Crypt_parts_spies)+
done




subsubsectionUnicity results for PMS, the pre-master-secret

textPMS determines B.
lemma Crypt_unique_PMS:
     "[| Crypt(pubK B)  (Nonce PMS)  parts (spies evs);
         Crypt(pubK B') (Nonce PMS)  parts (spies evs);
         Nonce PMS  analz (spies evs);
         evs  tls |]
      ==> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
apply (erule tls.induct, analz_mono_contra, force, simp_all (no_asm_simp))
txtFake, ClientKeyExch
apply blast+
done


(** It is frustrating that we need two versions of the unicity results.
    But Notes A ⦃Agent B, Nonce PMS⦄ determines both A and B.  Sometimes
    we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which
    determines B alone, and only if PMS is secret.
**)

textIn A's internal Note, PMS determines A and B.
lemma Notes_unique_PMS:
     "[| Notes A  Agent B,  Nonce PMS  set evs;
         Notes A' Agent B', Nonce PMS  set evs;
         evs  tls |]
      ==> A=A'  B=B'"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, force, simp_all)
txtClientKeyExch
apply (blast dest!: Notes_Crypt_parts_spies)
done


subsectionSecrecy Theorems

textKey compromise lemma needed to prove termanalz_image_keys.
  No collection of keys can help the spy get new private keys.
lemma analz_image_priK [rule_format]:
     "evs  tls
      ==> KK. (Key(priK B)  analz (Key`KK  (spies evs))) =
          (priK B  KK | B  bad)"
apply (erule tls.induct)
apply (simp_all (no_asm_simp)
                del: image_insert
                add: image_Un [THEN sym]
                     insert_Key_image Un_assoc [THEN sym])
txtFake
apply spy_analz
done


textslightly speeds up the big simplification below
lemma range_sessionkeys_not_priK:
     "KK  range sessionK  priK B  KK"
by blast


textLemma for the trivial direction of the if-and-only-if
lemma analz_image_keys_lemma:
     "(X  analz (G  H))  (X  analz H)  ==>
      (X  analz (G  H))  =  (X  analz H)"
by (blast intro: analz_mono [THEN subsetD])

(** Strangely, the following version doesn't work:
∀Z. (Nonce N ∈ analz (Key`(sessionK`Z) ∪ (spies evs))) =
    (Nonce N ∈ analz (spies evs))"
**)

lemma analz_image_keys [rule_format]:
     "evs  tls ==>
      KK. KK  range sessionK 
              (Nonce N  analz (Key`KK  (spies evs))) =
              (Nonce N  analz (spies evs))"
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (safe del: iffI)
apply (safe del: impI iffI intro!: analz_image_keys_lemma)
apply (simp_all (no_asm_simp)               (*faster*)
                del: image_insert imp_disjL (*reduces blow-up*)
                add: image_Un [THEN sym]  Un_assoc [THEN sym]
                     insert_Key_singleton
                     range_sessionkeys_not_priK analz_image_priK)
apply (simp_all add: insert_absorb)
txtFake
apply spy_analz
done

textKnowing some session keys is no help in getting new nonces
lemma analz_insert_key [simp]:
     "evs  tls ==>
      (Nonce N  analz (insert (Key (sessionK z)) (spies evs))) =
      (Nonce N  analz (spies evs))"
by (simp del: image_insert
         add: insert_Key_singleton analz_image_keys)


subsubsectionProtocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure

(** Some lemmas about session keys, comprising clientK and serverK **)


textLemma: session keys are never used if PMS is fresh.
  Nonces don't have to agree, allowing session resumption.
  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.
lemma PMS_lemma:
     "[| Nonce PMS  parts (spies evs);
         K = sessionK((Na, Nb, PRF(PMS,NA,NB)), role);
         evs  tls |]
   ==> Key K  parts (spies evs)  (Y. Crypt K Y  parts (spies evs))"
apply (erule rev_mp, erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB) 
apply (force, simp_all (no_asm_simp))
txtFake
apply (blast intro: parts_insertI)
txtSpyKeys
apply blast
txtMany others
apply (force dest!: Notes_Crypt_parts_spies Notes_master_imp_Crypt_PMS)+
done

lemma PMS_sessionK_not_spied:
     "[| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), role))  parts (spies evs);
         evs  tls |]
      ==> Nonce PMS  parts (spies evs)"
by (blast dest: PMS_lemma)

lemma PMS_Crypt_sessionK_not_spied:
     "[| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), role)) Y
            parts (spies evs);  evs  tls |]
      ==> Nonce PMS  parts (spies evs)"
by (blast dest: PMS_lemma)

textWrite keys are never sent if M (MASTER SECRET) is secure.
  Converse fails; betraying M doesn't force the keys to be sent!
  The strong Oops condition can be weakened later by unicity reasoning,
  with some effort.
  NO LONGER USED: see clientK_not_spied› and serverK_not_spied›
lemma sessionK_not_spied:
     "[| A. Says A Spy (Key (sessionK((NA,NB,M),role)))  set evs;
         Nonce M  analz (spies evs);  evs  tls |]
      ==> Key (sessionK((NA,NB,M),role))  parts (spies evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, analz_mono_contra)
apply (force, simp_all (no_asm_simp))
txtFake, SpyKeys
apply blast+
done


textIf A sends ClientKeyExch to an honest B, then the PMS will stay secret.
lemma Spy_not_see_PMS:
     "[| Notes A Agent B, Nonce PMS  set evs;
         evs  tls;  A  bad;  B  bad |]
      ==> Nonce PMS  analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
txtFake
apply spy_analz
txtSpyKeys
apply force
apply (simp_all add: insert_absorb) 
txtClientHello, ServerHello, ClientKeyExch: mostly freshness reasoning
apply (blast dest: Notes_Crypt_parts_spies)
apply (blast dest: Notes_Crypt_parts_spies)
apply (blast dest: Notes_Crypt_parts_spies)
txtClientAccepts and ServerAccepts: because termPMS  range PRF
apply force+
done


textIf A sends ClientKeyExch to an honest B, then the MASTER SECRET
  will stay secret.
lemma Spy_not_see_MS:
     "[| Notes A Agent B, Nonce PMS  set evs;
         evs  tls;  A  bad;  B  bad |]
      ==> Nonce (PRF(PMS,NA,NB))  analz (spies evs)"
apply (erule rev_mp, erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
txtFake
apply spy_analz
txtSpyKeys: by secrecy of the PMS, Spy cannot make the MS
apply (blast dest!: Spy_not_see_PMS)
apply (simp_all add: insert_absorb)
txtClientAccepts and ServerAccepts: because PMS was already visible;
  others, freshness etc.
apply (blast dest: Notes_Crypt_parts_spies Spy_not_see_PMS 
                   Notes_imp_knows_Spy [THEN analz.Inj])+
done



subsubsectionWeakening the Oops conditions for leakage of clientK

textIf A created PMS then nobody else (except the Spy in replays)
  would send a message using a clientK generated from that PMS.
lemma Says_clientK_unique:
     "[| Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y)  set evs;
         Notes A Agent B, Nonce PMS  set evs;
         evs  tls;  A'  Spy |]
      ==> A = A'"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all)
txtClientKeyExch
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
txtClientFinished, ClientResume: by unicity of PMS
apply (blast dest!: Notes_master_imp_Notes_PMS 
             intro: Notes_unique_PMS [THEN conjunct1])+
done


textIf A created PMS and has not leaked her clientK to the Spy,
  then it is completely secure: not even in parts!
lemma clientK_not_spied:
     "[| Notes A Agent B, Nonce PMS  set evs;
         Says A Spy (Key (clientK(Na,Nb,PRF(PMS,NA,NB))))  set evs;
         A  bad;  B  bad;
         evs  tls |]
      ==> Key (clientK(Na,Nb,PRF(PMS,NA,NB)))  parts (spies evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
txtClientKeyExch
apply blast 
txtSpyKeys
apply (blast dest!: Spy_not_see_MS)
txtClientKeyExch
apply (blast dest!: PMS_sessionK_not_spied)
txtOops
apply (blast intro: Says_clientK_unique)
done


subsubsectionWeakening the Oops conditions for leakage of serverK

textIf A created PMS for B, then nobody other than B or the Spy would
  send a message using a serverK generated from that PMS.
lemma Says_serverK_unique:
     "[| Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y)  set evs;
         Notes A Agent B, Nonce PMS  set evs;
         evs  tls;  A  bad;  B  bad;  B'  Spy |]
      ==> B = B'"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all)
txtClientKeyExch
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
txtServerResume, ServerFinished: by unicity of PMS
apply (blast dest!: Notes_master_imp_Crypt_PMS 
             dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
done


textIf A created PMS for B, and B has not leaked his serverK to the Spy,
  then it is completely secure: not even in parts!
lemma serverK_not_spied:
     "[| Notes A Agent B, Nonce PMS  set evs;
         Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB))))  set evs;
         A  bad;  B  bad;  evs  tls |]
      ==> Key (serverK(Na,Nb,PRF(PMS,NA,NB)))  parts (spies evs)"
apply (erule rev_mp, erule rev_mp)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
txtFake
apply blast 
txtSpyKeys
apply (blast dest!: Spy_not_see_MS)
txtClientKeyExch
apply (blast dest!: PMS_sessionK_not_spied)
txtOops
apply (blast intro: Says_serverK_unique)
done


subsubsectionProtocol goals: if A receives ServerFinished, then B is present
     and has used the quoted values PA, PB, etc.  Note that it is up to A
     to compare PA with what she originally sent.

textThe mention of her name (A) in X assures A that B knows who she is.
lemma TrustServerFinished [rule_format]:
     "[| X = Crypt (serverK(Na,Nb,M))
               (HashNumber SID, Nonce M,
                      Nonce Na, Number PA, Agent A,
                      Nonce Nb, Number PB, Agent B);
         M = PRF(PMS,NA,NB);
         evs  tls;  A  bad;  B  bad |]
      ==> Says B Spy (Key(serverK(Na,Nb,M)))  set evs 
          Notes A Agent B, Nonce PMS  set evs 
          X  parts (spies evs)  Says B A X  set evs"
apply (erule ssubst)+
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
txtFake: the Spy doesn't have the critical session key!
apply (blast dest: serverK_not_spied)
txtClientKeyExch
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
done

textThis version refers not to ServerFinished but to any message from B.
  We don't assume B has received CertVerify, and an intruder could
  have changed A's identity in all other messages, so we can't be sure
  that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
  to bind A's identity with PMS, then we could replace A' by A below.
lemma TrustServerMsg [rule_format]:
     "[| M = PRF(PMS,NA,NB);  evs  tls;  A  bad;  B  bad |]
      ==> Says B Spy (Key(serverK(Na,Nb,M)))  set evs 
          Notes A Agent B, Nonce PMS  set evs 
          Crypt (serverK(Na,Nb,M)) Y  parts (spies evs)  
          (A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y)  set evs)"
apply (erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp) add: ex_disj_distrib)
txtFake: the Spy doesn't have the critical session key!
apply (blast dest: serverK_not_spied)
txtClientKeyExch
apply (clarify, blast dest!: PMS_Crypt_sessionK_not_spied)
txtServerResume, ServerFinished: by unicity of PMS
apply (blast dest!: Notes_master_imp_Crypt_PMS 
             dest: Spy_not_see_PMS Notes_Crypt_parts_spies Crypt_unique_PMS)+
done


subsubsectionProtocol goal: if B receives any message encrypted with clientK
      then A has sent it

textASSUMING that A chose PMS.  Authentication is
     assumed here; B cannot verify it.  But if the message is
     ClientFinished, then B can then check the quoted values PA, PB, etc.

lemma TrustClientMsg [rule_format]:
     "[| M = PRF(PMS,NA,NB);  evs  tls;  A  bad;  B  bad |]
      ==> Says A Spy (Key(clientK(Na,Nb,M)))  set evs 
          Notes A Agent B, Nonce PMS  set evs 
          Crypt (clientK(Na,Nb,M)) Y  parts (spies evs) 
          Says A B (Crypt (clientK(Na,Nb,M)) Y)  set evs"
apply (erule ssubst)
apply (erule tls.induct, frule_tac [7] CX_KB_is_pubKB)
apply (force, simp_all (no_asm_simp))
txtFake: the Spy doesn't have the critical session key!
apply (blast dest: clientK_not_spied)
txtClientKeyExch
apply (blast dest!: PMS_Crypt_sessionK_not_spied)
txtClientFinished, ClientResume: by unicity of PMS
apply (blast dest!: Notes_master_imp_Notes_PMS dest: Notes_unique_PMS)+
done


subsubsectionProtocol goal: if B receives ClientFinished, and if B is able to
     check a CertVerify from A, then A has used the quoted
     values PA, PB, etc.  Even this one requires A to be uncompromised.
lemma AuthClientFinished:
     "[| M = PRF(PMS,NA,NB);
         Says A Spy (Key(clientK(Na,Nb,M)))  set evs;
         Says A' B (Crypt (clientK(Na,Nb,M)) Y)  set evs;
         certificate A KA  parts (spies evs);
         Says A'' B (Crypt (invKey KA) (Hashnb, Agent B, Nonce PMS))
            set evs;
         evs  tls;  A  bad;  B  bad |]
      ==> Says A B (Crypt (clientK(Na,Nb,M)) Y)  set evs"
by (blast intro!: TrustClientMsg UseCertVerify)

(*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
(*30/9/97: loads in 476s, after removing unused theorems*)
(*30/9/97: loads in 448s, after fixing ServerResume*)

(*08/9/97: loads in 189s (pike), after much reorganization,
           back to 621s on albatross?*)

(*10/2/99: loads in 139s (pike)
           down to 433s on albatross*)

(*5/5/01: conversion to Isar script
          loads in 137s (perch)
          the last ML version loaded in 122s on perch, a 600MHz machine:
                twice as fast as pike.  No idea why it's so much slower!
          The Isar script is slower still, perhaps because simp_all simplifies
          the assumptions be default.
*)

(*20/11/11: loads in 5.8s elapses time, 9.3s CPU time on dual-core laptop*)

end