<commit_before>(*  Title:      HOL/Auth/CertifiedEmail
    ID:         $Id$
    Author:     <NAME>, <NAME> and <NAME>
*)

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

theory CertifiedEmail = Public:

syntax
  TTP        :: agent
  RPwd       :: "agent => key"

translations
  "TTP"   == "Server "
  "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.*}
constdefs
  "response"    :: "agent => agent => nat => msg"
   "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"


consts  certified_mail   :: "event list set"
inductive "certified_mail"
  intros 

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'}.
         He replies over the established SSL channel.*}
 "[|evs3 \<in> certified_mail;
    Notes TTP {|Agent R', Agent TTP, S2TTP'', Key(RPwd R'), hr'|} \<in> set evs3;
    S2TTP'' = Crypt (pubEK TTP) 
                     {|Agent S, Number BothAuth, Key k', Agent R', hs'|};
    TTP \<noteq> R';  hs' = hr';  k' \<in> symKeys|]
 ==> 
  Notes R' {|Agent TTP, Agent R', Key k', hr'|} # 
  Gets S (Crypt (priSK TTP) S2TTP'') # 
  Says TTP S (Crypt (priSK TTP) S2TTP'') # evs3 \<in> certified_mail"

Reception:
 "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
  ==> Gets B X#evsr \<in> certified_mail"


declare Says_imp_knows_Spy [THEN analz.Inj, dest]
declare analz_into_parts [dest]

(*A "possibility property": there are traces that reach the end*)<commit_msg>removal of prime characters<commit_after>(*  Title:      HOL/Auth/CertifiedEmail
    ID:         $Id$
    Author:     <NAME>, <NAME> and <NAME>
*)

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

theory CertifiedEmail = Public:

syntax
  TTP        :: agent
  RPwd       :: "agent => key"

translations
  "TTP"   == "Server "
  "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.*}
constdefs
  "response"    :: "agent => agent => nat => msg"
   "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}"


consts  certified_mail   :: "event list set"
inductive "certified_mail"
  intros 

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}.
         He replies over the established SSL channel.*}
 "[|evs3 \<in> certified_mail;
    Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} \<in> set evs3;
    S2TTP = Crypt (pubEK TTP) 
                     {|Agent S, Number BothAuth, Key k, Agent R, hs|};
    TTP \<noteq> R;  hs = hr;  k \<in> symKeys|]
 ==> 
  Notes R {|Agent TTP, Agent R, Key k, hr|} # 
  Gets S (Crypt (priSK TTP) S2TTP) # 
  Says TTP S (Crypt (priSK TTP) S2TTP) # evs3 \<in> certified_mail"

Reception:
 "[|evsr \<in> certified_mail; Says A B X \<in> set evsr|]
  ==> Gets B X#evsr \<in> certified_mail"


declare Says_imp_knows_Spy [THEN analz.Inj, dest]
declare analz_into_parts [dest]

(*A "possibility property": there are traces that reach the end*)
{'fraction_non_alphanumeric': 0.13574920908829452, 'fraction_numerical': 0.006902502157031924, 'mean_word_length': 2.9472190692395004, 'pattern_counts': {'":': 2, '<': 57, '<?xml version=': 0, '>': 77, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4376735', 'n_tokens_mistral': 2581, 'n_tokens_neox': 2396, 'n_words': 942}