Modeling and Proving Cryptographic Security in F*

Basic Security Background

The Setting

• S, R, and A are all programs sharing a communication channel

• A is typically a polynomially bounded computational entity

  • Can intercept and tamper with messages on the wire

  Sender (S)   ------network-------->  Receiver (R)
                        ^
                        |
                        |
                        v
                   Adversary (A)

• Want to make security claims that cover authenticity and secrecy

Authenticity

When R accepts a message m from S only when S actually sent m

• Correpondence assertions on traces of events
  • Event: S:send m or R:receive m
  • Trace: Sequence of events
  • Authenticity: every R:receive m event in a trace is preceded by a S:send m

Secrecy

No information about any secrets sent by S is leaked to A

• Secrecy: Usually an equivalence relation on traces
  • Messages observed by A are independent of the secrets
• In terms of language-based information-flow securuty

val sender (secret:bytes) (public:bytes) : bytes

let no_leakage = forall s0 s1 p. sender s0 p == sender s1 p

Perfect Secrecy and Authenticity: Unattainable

• S cannot communicate anything useful about its secret to the R if the messages carries no information about R!

• But, using cryptography, we can prove probabilistic security guarantees

Cryptographic Games and Hypotheses

• A game G is a program with several procedures and shared state

• Adversary A interacts with G

• A wins if they get G some procedure to emit a specific result (e.g., true)

• Goal: Show that the probability of A winning is low

IND-CPA: INDistinguishability under Chosen-Plaintext Attacks

• Secrecy property for encryption schemes

  • Ciphertext leaks only a negligible amount of the plain text

  let ind_cpa (encrypt : key -> msg -> cipher) =
  
  (* A secret key and secret bit *)
  let key = sample_random_key () in
  let b : bool = random_sample_bit () in
  
  (* Encrypt either message, depending on the bit *)
  let left_or_right (m0, m1) =
      if b
      then encrypt key m0
      else encrypt key m1 in
  
  (* Check the attacker's guess *)
  let check guess = b=guess in
  
  left_or_right,
  check

• Attacker's advantage is the probability of guessing right more than half the time

IND-CPA as an Ideal Functionality

• The definition of IND-CPA is meant to be self-evidently useful notion of ciphertext indistinguishability

• Sometimes, it is possible to prove semantic security (like IND-CPA) of some encryption schemes based on other assumptions

  • E.g., Based on based on the Decisional Diffie-Hellman, El Gamal encryption is semantically secure

• But, this is out of scope for us

• Usually, one assumes that certain schemes (e.g., AES with IVs) are -IND-CPA, for some symbolic

UF-CMA: UnForgeability under Chosen-Message Attacks

An authenticity property for Message-Authentication Codes (MACs)

• A MAC: t = mac m k could only be effectively produced through knowledge of the secret key k, i.e., t cannot be forged.

• Authentication by “log lookup”: -UF-CMA secure if the probability of an adversary forging a tag is .

let uf_cma (mac: key -> msg -> tag, verify: key -> msg -> tag -> bool) =x
    (* Sample a random key *)
    let k = sample_random_key () in
    (* Allocate a log *)
    let log : ref (list (msg * tag)) = alloc [] in
    (* mac wrapper: call mac and log it *)
    let mac (m:msg) =
        let t = mac m k in
        log := (m, t) :: !log;
        t in
    (* verify wrapper: correct verify using the log *)
    let verify (m:msg) (t:tag) =
        let b = verify k m t in
        b && (m, t) `not-in` !log in
    mac, verify

Our goal: Authenticated Encryption

• Given an -IND-CPA encryption scheme and a -UF-CMA MAC

We want

• ae_enc that:

  • Encrypts the plain text
  • MACs the cipher text
  • Concatenates the result

• ae_dec that:

  • Checks the MAC of the cipher
  • Decrypts only authenticated ciphers

• And prove that it is semantically secure with an advantage proportionate to

Modeling Crypto Games in F*

HMAC-SHA1

• HMAC: Bellare, Cannetti, Krawczyk

• HMAC-SHA1 as a total function in F*

let hmac_sha1 (k:sha1_key) (m:msg) : tag =
  let x5c = byte_of_int 92 in
  let x36 = byte_of_int 54 in
  let opad = Seq.create blocksize x5c in
  let ipad = Seq.create blocksize x36 in
  let xor_key_opad = xor keysize k opad in
  let xor_key_ipad = xor keysize k ipad in
  sha1 (xor_key_opad `Seq.append`
       (sha1 (xor_key_ipad `Seq.append` m)))

• We're going to assume that HMAC-SHA1 is -UF-CMA secure

• But, how best to state that assumption?

Idealization flags

• Write the concrete and ideal versions of a crypto functionality together

let mac_verify () = 
    let key = sample_random_key ()
    let log = ref [] in

    let mac k m = 
        let t = hmac_sha1 k m in
        if Flag.idealizing uf_cma (* BRANCHING HERE IS A CRYPTO HYPOTHESIS *)
        then log := (m, t) :: !log; 
        t
    in
        
    let verify k m t =
        let ok = (t = hmac_sha1 k m) in
        if Flag.idealizing uf_cma (* BRANCHING HERE IS A CRYPTO HYPOTHESIS *)
        then ok && (!log `contains` (m, t))
        else ok
    in
    
    mac, verify

• mac_verify[uf_cma=true] mac_verify[uf_cma=false]

Sequences of Games: Multiple Idealizations

concrete_ae 
=
ae [ideal_ae=false]
=
mac_verify[uf_cma=false] . enc_dec[ind_cpa=false]
~_e
mac_verify[uf_cma=true] . enc_dec[ind_cpa=false]
~_e'
mac_verify[uf_cma=true] . enc_dec[ind_cpa=true]
=
ae [ideal_ae=true]

Aside: Secrecy as Parametricity

• val f : 'a -> 'a. What is (f 0)?

• val g : 'a -> int. What is (g 0)? What is (g 1)?

• Well-typed code gains no information about its parametrically typed arguments

Secrecy as Parametricity, with modules

module Plain
val plain : Type

module Client
val f : plain -> int

• What is Client.f p?
  • Not sure, but it's the same as Client.f q

Modeling confidential plaintexts

• An abstract type of plaintexts Plain.plain

module Plain

val plain : Type

val repr (p:plain{not ind_cpa}) : bytes (* cannot break confidentiality if ind_cpa *)

val coerce (b:bytes{not uf_cma}) : plain (* cannot break integrity if uf_cma *)

• With a function repr that allows breaking confidentiality
  • But only when not idealizing for secrecy (i.e. ideal_ind_cpa = false)
• With a function coerce that allows breaking integrity
  • But only when not idealizing for authenticity (i.e. ideal_uf_cma = false)

IND-CPA in F*

• Encryption of zeroes; decryption by table lookup

let ind_cpa () =
    let key = sample_random_key () in
    let log = ref [] in
    
    let encrypt (p:Plain.plain) : bytes = 
        let q = 
            if Idealizing.ind_cpa (*!!! AUDIT, Crypto Hypothesis *)
            then zeroes
            else Plain.repr p
        in
        let cipher = encrypt key q in
        if ideal_ind_cpa (*!!! AUDIT, Crypto Hypothesis *)
        then log := (p, cipher)::!log;
        cipher
    in
    
    (* MEANT TO BE USED ONLY WITH AUTHENTIC CIPHERS *)
    let decrypt (c:cipher) : option Plain.plain =
        let q = decrypt key c in
        if Idealizing.ind_cpa  (*!!! AUDIT, Crypto Hypothesis *)
        then match find !log (fun (_, c') -> c=c') with
             | None -> None
             | Some (p, _) -> Some p
        ...

Streaming Authenticated Encryption

StreamAE Verification