LabeledPKI.fst

/// LabeledPKI (implementation)
/// ============================
module LabeledPKI

module A = LabeledCryptoAPI
module R = LabeledRuntimeAPI

let serialize_session_st st : bytes =
   match st with
   |SigningKey t secret_key -> concat ((string_to_bytes "SigningKey")) (concat ((string_to_bytes t)) (secret_key))
   |VerificationKey t p public_key -> concat ((string_to_bytes "VerificationKey")) (concat ((string_to_bytes t)) (concat ((string_to_bytes p)) public_key))
   |DHPrivateKey t secret_key -> concat ((string_to_bytes "DHPrivateKey")) (concat ((string_to_bytes t)) secret_key)
   |DHPublicKey t p public_key -> concat ((string_to_bytes "DHPublicKey")) (concat ((string_to_bytes t)) (concat ((string_to_bytes p)) public_key))
   |OneTimeDHPrivKey t secret_key -> concat ((string_to_bytes "OneTimeDHPrivKey")) (concat ((string_to_bytes t)) secret_key)
   |OneTimeDHPubKey t p public_key -> concat ((string_to_bytes "OneTimeDHPubKey")) (concat ((string_to_bytes t)) (concat ((string_to_bytes p)) public_key))
   |DeletedOneTimeKey t -> concat ((string_to_bytes "DeletedOneTimeKey")) ((string_to_bytes t))
   |DecryptionKey t secret_key -> concat ((string_to_bytes "DecryptionKey")) (concat ((string_to_bytes t)) secret_key)
   |EncryptionKey t p public_key -> concat ((string_to_bytes "EncryptionKey")) (concat ((string_to_bytes t)) (concat ((string_to_bytes p)) public_key))
   |APP s -> concat ((string_to_bytes "APP")) s

let parse_session_st (serialized_session:bytes) : result session_st =
  let? r = split serialized_session in
  let (tn,o) = r in
  match? bytes_to_string tn with
  | "APP" -> Success (APP o)
  | "SigningKey" -> (
    let? (tb,sk) = split o in
    let? t = bytes_to_string tb in
    Success (SigningKey t sk))
  | "VerificationKey" -> (
    let? (tb,ppk) = split o in
    let? t = bytes_to_string tb in
    let? (pb,pk) = split ppk in
    let? p = bytes_to_string pb in
    Success (VerificationKey t p pk))
  | "DHPrivateKey" -> (
    let? (tb,sk) = split o in
    let? t = bytes_to_string tb in
    Success (DHPrivateKey t sk))
  | "DHPublicKey" -> (
    let? (tb,ppk) = split o in
    let? t = bytes_to_string tb in
    let? (pb,pk) = split ppk in
    let? p = bytes_to_string pb in
    Success (DHPublicKey t p pk))
  | "OneTimeDHPrivKey" -> (
    let? (tb,sk) = split o in
    let? t = bytes_to_string tb in
    Success (OneTimeDHPrivKey t sk))
  | "OneTimeDHPubKey" -> (
    let? (tb,ppk) = split o in
    let? t = bytes_to_string tb in
    let? (pb,pk) = split ppk in
    let? p = bytes_to_string pb in
    Success (OneTimeDHPubKey t p pk))
  | "DeletedOneTimeKey" -> (
    let? t = bytes_to_string o in
    Success (DeletedOneTimeKey t))
  | "DecryptionKey" -> (
    let? (tb,sk) = split o in
    let? t = bytes_to_string tb in
    Success (DecryptionKey t sk))
  | "EncryptionKey" -> (
    let? (tb,ppk) = split o in
    let? t = bytes_to_string tb in
    let? (pb,pk) = split ppk in
    let? p = bytes_to_string pb in
    Success (EncryptionKey t p pk))
  | _ -> Error "unknown key name"


val parse_serialize_session_st_lemma : ss:session_st ->
    Lemma (Success ss == parse_session_st (serialize_session_st ss))
          [SMTPat (parse_session_st (serialize_session_st ss))]
let parse_serialize_session_st_lemma ss =
  assert_norm(Success ss == parse_session_st (serialize_session_st ss))


let valid_session (pr:R.preds) (i:timestamp) (p:principal) (si:nat) (vi:nat) (st:session_st) : Type0 =
  match st with
  | SigningKey t secret_key ->
    A.is_signing_key pr.R.global_usage i secret_key (readers [P p]) t
  | VerificationKey t p public_key ->
    A.is_verification_key pr.R.global_usage i public_key (readers [P p]) t
  | DHPrivateKey t secret_key ->
    A.is_dh_private_key pr.R.global_usage i secret_key (readers [P p]) t
  | DHPublicKey t p public_key ->
    A.is_dh_public_key pr.R.global_usage i public_key (readers [P p]) t
  | OneTimeDHPrivKey t secret_key ->
    vi = 0 /\ A.is_dh_private_key pr.R.global_usage i secret_key (readers [V p si 0]) t
  | OneTimeDHPubKey t p public_key ->
    (exists si. A.is_dh_public_key pr.R.global_usage i public_key (readers [V p si 0]) t)
  | DeletedOneTimeKey t ->
    vi = 1
  | DecryptionKey t secret_key ->
    A.is_private_dec_key pr.R.global_usage i secret_key (readers [P p]) t
  | EncryptionKey t p public_key ->
    A.is_public_enc_key pr.R.global_usage i public_key (readers [P p]) t
  | APP s -> R.(pr.trace_preds.session_st_inv i p si vi s)

val valid_session_later: pr:R.preds -> i:timestamp -> j:timestamp -> p: principal -> si:nat -> vi:nat -> st:session_st -> Lemma
  ((valid_session pr i p si vi st /\ later_than j i) ==> valid_session pr j p si vi st)
  [SMTPat (valid_session pr i p si vi st); SMTPat (valid_session pr j p si vi st)]
let valid_session_later pr i j p si vi st = ()

let includes_lemma (p:principal) (s:nat) (v:nat) : Lemma (includes_ids [P p] [V p s v]) [SMTPat (includes_ids [P p] [V p s v])] = ()

val valid_session_lemma: pr:R.preds -> i:timestamp -> p: principal -> si:nat -> vi:nat -> st:session_st ->
  Lemma (requires (valid_session pr i p si vi st))
        (ensures (A.is_msg pr.R.global_usage i (serialize_session_st st) (readers [V p si vi])))
        [SMTPatOr
          [
            [SMTPat (valid_session pr i p si vi st)];
            [SMTPat (A.is_msg pr.R.global_usage i (serialize_session_st st) (readers [V p si vi]))]
          ]
        ]
let valid_session_lemma pr i p si vi st =
  let l = readers [V p si vi] in
  let tg : A.msg pr.R.global_usage i public =
    match st with
    | SigningKey _ _ -> A.string_to_bytes #pr.R.global_usage #i ("SigningKey")
    | VerificationKey _ _ _ -> A.string_to_bytes #pr.R.global_usage #i ("VerificationKey")
    | DHPrivateKey _ _ -> A.string_to_bytes #pr.R.global_usage #i ("DHPrivateKey")
    | DHPublicKey _ _ _ -> A.string_to_bytes #pr.R.global_usage #i ("DHPublicKey")
    | OneTimeDHPrivKey _ _ -> A.string_to_bytes #pr.R.global_usage #i ("OneTimeDHPrivKey")
    | OneTimeDHPubKey _ _ _ -> A.string_to_bytes #pr.R.global_usage #i ("OneTimeDHPubKey")
    | DeletedOneTimeKey _ -> A.string_to_bytes #pr.R.global_usage #i ("DeletedOneTimeKey")
    | DecryptionKey _ _ -> A.string_to_bytes #pr.R.global_usage #i ("DecryptionKey")
    | EncryptionKey _ _ _ -> A.string_to_bytes #pr.R.global_usage #i ("EncryptionKey")
    | APP _ -> A.string_to_bytes #pr.R.global_usage #i ("APP") in
  match st with
  | SigningKey t secret_key
  | DHPrivateKey t secret_key
  | DecryptionKey t secret_key ->
    assert (A.can_flow i public l);
    A.includes_can_flow_lemma i [P p] [V p si vi];
    let ct = A.concat #pr.R.global_usage #i #(readers [P p]) tg (A.concat #pr.R.global_usage #i #(readers [P p]) (A.string_to_bytes #pr.R.global_usage #i t) secret_key) in
    ()
  | OneTimeDHPrivKey t secret_key ->
    let ct = A.concat #pr.R.global_usage #i #(readers [V p si vi]) tg (A.concat #pr.R.global_usage #i #(readers [V p si vi]) (A.string_to_bytes #pr.R.global_usage #i t) secret_key) in
    ()
  | OneTimeDHPubKey t p' public_key ->
    let pb = A.string_to_bytes #pr.R.global_usage #i (p') in
    let ct = A.concat #pr.R.global_usage #i #l tg (A.concat #pr.R.global_usage #i #l (A.string_to_bytes #pr.R.global_usage #i t) (A.concat #pr.R.global_usage #i #l pb public_key)) in
    ()
  | DeletedOneTimeKey t ->
    let ct = A.concat #pr.R.global_usage #i #(readers [V p si vi]) tg (A.string_to_bytes #pr.R.global_usage #i t) in
    ()
  | VerificationKey t p' public_key
  | DHPublicKey t p' public_key
  | EncryptionKey t p' public_key ->
    let pb = A.string_to_bytes #pr.R.global_usage #i (p') in
    assert (A.can_flow i public (readers [P p]));
    A.includes_can_flow_lemma i [P p] [V p si vi];
    let ct = A.concat #pr.R.global_usage #i #l tg (A.concat #pr.R.global_usage #i #l (A.string_to_bytes #pr.R.global_usage #i t) (A.concat #pr.R.global_usage #i #l pb public_key)) in
    ()
  | APP s ->
    R.(pr.trace_preds.session_st_inv_lemma i p si vi s);
    assert (A.is_msg pr.R.global_usage i s l);
    let ct = A.concat #pr.R.global_usage #i #l tg s in
    ()


let session_st_inv pr i p si vi st: prop =
  A.is_msg pr.R.global_usage i st (readers [V p si vi]) /\
  (match parse_session_st st with
   | Success s -> valid_session pr i p si vi s
   | _ -> False)

val session_st_inv_later: pr:R.preds -> i:timestamp -> j:timestamp -> p: principal -> si:nat -> vi:nat -> st:bytes -> Lemma
  ((session_st_inv pr i p si vi st /\ later_than j i) ==> session_st_inv pr j p si vi st)
  [SMTPat (session_st_inv pr i p si vi st); SMTPat (session_st_inv pr j p si vi st)]
let session_st_inv_later pr i j p si vi st = ()

let pki (pr:R.preds) : R.preds = {
  R.global_usage = pr.R.global_usage;
  R.trace_preds = {
    R.can_trigger_event = pr.R.trace_preds.R.can_trigger_event;
    R.session_st_inv = session_st_inv pr;
    R.session_st_inv_later = session_st_inv_later pr;
    R.session_st_inv_lemma = (fun i p si vi st -> ())
  }
}

open LabeledCryptoAPI
open LabeledRuntimeAPI
let new_session #pr #i p si vi ss =
  let sst = serialize_session_st (APP ss) in
  assert (session_st_inv pr i p si vi sst);
  assert ((pki pr).trace_preds.session_st_inv i p si vi sst);
  new_session #(pki pr) #i p si vi sst

let update_session #pr #i p si vi ss =
  let sst = serialize_session_st (APP ss) in
  update_session #(pki pr) #i p si vi sst

let get_session #pr #i p si =
  let (|vi,s|) = get_session #(pki pr) #i p si in
  match parse_session_st s with
  | Success (APP s') ->
    assert (valid_session pr  i p si vi (APP s'));
    pr.trace_preds.session_st_inv_lemma i p si vi s';
    (|vi,s'|)
  | _ -> error "get_session: not an application state"

let find_session #pr #i p f =
  let f' si vi st =
    match parse_session_st st with
    | Success (APP s) -> f si vi s
    | _ -> false in
  match find_session #(pki pr) #i p f' with
  | None -> None
  | Some (|si,vi,st|) -> (
    (match parse_session_st st with
     | Success (APP s') ->
       assert (valid_session pr i p si vi (APP s'));
       pr.trace_preds.session_st_inv_lemma i p si vi s';
       Some (|si,vi,s'|)
     | _ -> error "find_session: not an application state")
)

let keygen pr p si kt ts :
  LCrypto (t:timestamp & private_key pr t si p kt ts) (pki pr)
  (requires (fun _ -> True))
  (ensures (fun t0 (|t,sk|) t1 -> t == trace_len t0 /\ trace_len t1 == t + 1)) =
  match kt with
  | SIG -> let (|t,sk|) = R.rand_gen #(pki pr) (readers [P p]) (sig_usage ts) in (|t,sk|)
  | DH -> let (|t,sk|) = R.rand_gen #(pki pr) (readers [P p]) (dh_usage ts) in (|t,sk|)
  | PKE -> let (|t,sk|) =  R.rand_gen #(pki pr) (readers [P p]) (pke_usage ts) in (|t,sk|)
  | OneTimeDH -> let (|t,sk|) =  R.rand_gen #(pki pr) (readers [V p si 0]) (dh_usage ts) in (|t,sk|)

let private_key_st pr i p si vi (kt:key_type{kt <> OneTimeDH}) ts (sk:private_key pr i si p kt ts) : s:session_st {valid_session pr i p si vi s}  =
  match kt with
  | SIG -> SigningKey ts sk
  | DH -> DHPrivateKey ts sk
  | PKE -> DecryptionKey ts sk

let public_key_st pr i p peer si vi (kt:key_type{kt <> OneTimeDH}) ts (sk:private_key pr i si p kt ts) : s:session_st {valid_session pr i peer si vi s}  =
  match kt with
  | SIG -> VerificationKey ts p (A.vk #pr.global_usage #i #(readers [P p]) sk)
  | DH -> DHPublicKey ts p (A.dh_pk #pr.global_usage #i #(readers [P p]) sk)
  | PKE -> EncryptionKey ts p (A.pk #pr.global_usage #i #(readers [P p]) sk)

let kt2string (kt:key_type) =
  match kt with
  | SIG -> "SIG"
  | DH -> "DH"
  | PKE -> "PKE"
  | OneTimeDH -> "OneTimeDH"

let gen_private_key #pr #t0 p kt ts =
  print_string ("generating private key '"^ts^"' of type "^(kt2string kt)^" for '"^p^"'\n");
  let si = new_session_number #(pki pr) p in
  let (|t1,sk|) = keygen pr p si kt ts in
  assert (later_than t1 t0);
  let st = (match kt with | OneTimeDH -> OneTimeDHPrivKey ts sk | _ -> private_key_st pr t1 p si 0 kt ts sk) in
  let new_ss_st = serialize_session_st st in
  let t2 = global_timestamp () in
  assert (session_st_inv pr t2 p si 0 new_ss_st);
  assert ((pki pr).trace_preds.session_st_inv t2 p si 0 new_ss_st);
  LabeledRuntimeAPI.new_session #(pki pr) #t2 p si 0 new_ss_st;
  si

let get_private_key #pr #i p kt ts =
  let filter si vi b = match kt, parse_session_st b with
    | SIG, Success (SigningKey ts' sk)
    | DH, Success (DHPrivateKey ts' sk)
    | PKE, Success (DecryptionKey ts' sk)
    | OneTimeDH, Success (OneTimeDHPrivKey ts' sk) -> ts = ts'
    | _ -> false in
  match R.find_session #(pki pr) #i p filter with
  | Some (|si,vi,st|) ->
    (match kt, parse_session_st st with
     | SIG, Success (SigningKey ts' sk) -> (|si, sk|)
     | DH, Success (DHPrivateKey ts' sk) -> (|si, sk|)
     | PKE, Success (DecryptionKey ts' sk) -> (|si, sk|)
     | OneTimeDH, Success (OneTimeDHPrivKey ts' sk) -> (|si, sk|)
     |_ -> error "not the right kind of key")
  | None -> error ("private key named '" ^ ts ^ "' not found in " ^ p ^ "'s state")

let install_public_key #pr #i p peer kt ts =
  print_string ("installing public key for "^p^" at "^peer^"\n");
  let (|osi, sk|) = get_private_key #pr #i p kt ts in
  let si = new_session_number #(pki pr) peer in
  let st = (match kt with | OneTimeDH -> OneTimeDHPubKey ts p (A.dh_pk #pr.global_usage #i #(readers [V p osi 0]) sk) | _ -> public_key_st pr i p peer si 0 kt ts sk) in
  let new_st = serialize_session_st st in
  R.new_session #(pki pr) #i peer si 0 new_st;
  si

let get_public_key #pr #i p peer kt ts =
  let filter si vi b = match kt, parse_session_st b with
    | SIG, Success (VerificationKey ts' pr _)
    | DH, Success (DHPublicKey ts' pr _)
    | PKE, Success (EncryptionKey ts' pr _)
    | OneTimeDH, Success (OneTimeDHPubKey ts' pr _) -> pr = peer && ts = ts'
    | _ -> false in
  match R.find_session #(pki pr) #i p filter with
  | Some (|si,vi,st|) ->
    (match kt, parse_session_st st with
     | SIG, Success (VerificationKey ts' _ sk) -> sk
     | DH, Success (DHPublicKey ts' _ sk) -> sk
     | PKE, Success (EncryptionKey ts' _ sk) -> sk
     | OneTimeDH, Success (OneTimeDHPubKey ts' peer sk) -> sk
     |_ -> error "not the right kind of key")
  | None -> error ("Could not find " ^ peer ^ "'s public key (with name " ^ ts ^ ") in " ^ p ^ "'s state")

let delete_one_time_key #pr #i p ts =
  let (|si, sk|) = get_private_key #pr #i p OneTimeDH ts in
  let st = serialize_session_st (DeletedOneTimeKey ts) in
  R.update_session #(pki pr) #i p si 1 st