src/HOL/Auth/CertifiedEmail.thy

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

(*  Title:      HOL/Auth/CertifiedEmail.thy
    Author:     Giampaolo Bella, Christiano Longo and Lawrence C Paulson
*)

header{*The Certified Electronic Mail Protocol by Abadi et al.*}

theory CertifiedEmail imports Public begin

abbreviation
  TTP :: agent where
  "TTP == Server"

abbreviation
  RPwd :: "agent => key" where
  "RPwd == shrK"

 
(*FIXME: the four options should be represented by pairs of 0 or 1.
  Right now only BothAuth is modelled.*)
consts
  NoAuth   :: nat
  TTPAuth  :: nat
  SAuth    :: nat
  BothAuth :: nat

text{*We formalize a fixed way of computing responses.  Could be better.*}
definition "response" :: "agent => agent => nat => msg" where
   "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"


inductive_set certified_mail :: "event list set"
  where

  Nil: --{*The empty trace*}
     "[] \<in> certified_mail"

| Fake: --{*The Spy may say anything he can say.  The sender field is correct,
          but agents don't use that information.*}
      "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] 
       ==> Says Spy B X # evsf \<in> certified_mail"

| FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
    equipped with the necessary credentials to serve as an SSL server.*}
         "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
          ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"

| CM1: --{*The sender approaches the recipient.  The message is a number.*}
 "[|evs1 \<in> certified_mail;
    Key K \<notin> used evs1;
    K \<in> symKeys;
    Nonce q \<notin> used evs1;
    hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|};
    S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|]
  ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, 
                 Number cleartext, Nonce q, S2TTP|} # evs1 
        \<in> certified_mail"

| CM2: --{*The recipient records @{term S2TTP} while transmitting it and her
     password to @{term TTP} over an SSL channel.*}
 "[|evs2 \<in> certified_mail;
    Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, 
             Nonce q, S2TTP|} \<in> set evs2;
    TTP \<noteq> R;  
    hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |]
  ==> 
   Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2
      \<in> certified_mail"

| CM3: --{*@{term TTP} simultaneously reveals the key to the recipient and gives
         a receipt to the sender.  The SSL channel does not authenticate 
         the client (@{term R}), but @{term TTP} accepts the message only 
         if the given password is that of the claimed sender, @{term R}.