clutch.approxis.examples.symmetric_init

From clutch.approxis Require Import approxis map list linked_list.
From clutch.approxis Require Export bounded_oracle.
Set Default Proof Using "Type*".

Section symmetric.

  Context `{approxisRGS Σ}.

A symmetric encryption scheme is given by three functions (keygen, encrypt, decrypt).
The set of keys, messages, and ciphertexts are modelled by finite sets of integers 0, Key, 0, Input, and 0, Output.

  Class SYM_init_params :=
    { card_key : nat
    ; card_message : nat
    ; card_cipher : nat
    ; sym_params : val := (#card_key, #card_message, #card_cipher) }.

  (* Variable Key Message Cipher : nat. *)

  (* Let keygen scheme : expr := Fst scheme.
     Let enc scheme : expr := Fst (Snd scheme).
     Let rand_cipher scheme : expr := Snd (Snd scheme). *)

  Definition get_param_card_key : val := λ:"sym_params", Fst (Fst "sym_params").
  Definition get_param_card_message : val := λ:"sym_params", Snd (Fst "sym_params").
  Definition get_param_card_cipher : val := λ:"sym_params", Snd "sym_params".

  (* rand_cipher is currently unused ; it would be useful if a SYM module had
   abstract types. *)
  (* enc_scheme can be any expression that reduces to a triplet of the form:
  `(keygen, (enc, dec))*)
  Class SYM_init `{SYM_init_params} :=
    { keygen : val
    ; enc_scheme : expr
    ; rand_cipher : val
    ; sym_scheme : val := (sym_params, (keygen, λ: <>, enc_scheme), rand_cipher)%V
    }.

  (* `get_keygen`, `get_enc` and `get_dec` shoudl now be called with an
   encryption scheme i.e. only the tuple of these three, this ensures
   the state is shared between them *)
  Definition get_params : val := λ:"sym_scheme", Fst (Fst "sym_scheme").
  Definition get_card_key : val := λ:"sym_scheme", Fst (Fst (Fst (Fst "sym_scheme"))).
  Definition get_card_message : val := λ:"sym_scheme", Snd (Fst (Fst (Fst "sym_scheme"))).
  Definition get_card_cipher : val := λ:"sym_scheme", Snd (Fst "sym_scheme").
  Definition get_enc_scheme : val := λ:"sym_scheme", Snd (Snd (Fst "sym_scheme")).
  Definition get_keygen : val := λ:"sym_scheme", Fst (Snd (Fst "sym_scheme")).
  Definition get_enc : val := λ:"enc_scheme", Fst "enc_scheme".
  Definition get_dec : val := λ:"enc_scheme", Snd "enc_scheme".
  Definition get_rand_cipher : val := λ:"sym_scheme", Snd "sym_scheme".

  Section CPA.

Indistinguishability of Chosen Plaintext Attacks security for symmetric/private key encryption.
Real vs random variant (sometimes called "CPA

    Definition CPA : val :=
      λ:"b" "adv" "scheme" "Q",
        let: "rr_key_b" :=
          let: "enc_scheme" := get_enc_scheme "scheme" #() in
          let: "key" := get_keygen "scheme" #() in
          (* let: "enc_key" := enc "scheme" "key" in *)
          if: "b" then
            (* "enc_key" *)
            get_enc "enc_scheme" "key"
          else
            get_rand_cipher "scheme" in
        let: "oracle" := q_calls (get_card_message "scheme") "Q" "rr_key_b" in
        let: "b'" := "adv" "oracle" in
        "b'".

    Definition CPA_real : val :=
      λ:"scheme" "Q",
        let: "enc_scheme" := get_enc_scheme "scheme" #() in
        let: "key" := get_keygen "scheme" #() in
        q_calls (get_card_message "scheme") "Q" (get_enc "enc_scheme" "key").

    (* TODO this should just use `rand` instead of get_rand_cipher. *)
    Definition CPA_rand : val :=
      λ:"scheme" "Q",
        q_calls (get_card_message "scheme") "Q" (get_rand_cipher "scheme").

  End CPA.

End symmetric.

Module CPA_sem.

  Definition CPA_real : val :=
    λ:"scheme" "Q",
      let: "enc_scheme" := get_enc_scheme "scheme" #() in
      let: "key" := get_keygen "scheme" #() in
      q_calls_poly #() #() "Q" (get_enc "enc_scheme" "key").

  (* TODO this should just use `rand` instead of get_rand_cipher. *)
  Definition CPA_rand : val :=
    λ:"scheme" "Q",
      q_calls_poly #() #() "Q" (get_rand_cipher "scheme").

End CPA_sem.

  Section CCA.

Indistinguishability of Chosen Ciphertext Attacks security for symmetric/private key encryption.
Left vs Right (sometimes called "CCA").
References:
  • Definition 9.1, Mike Rosulek, 2020, The Joy of Cryptography.
  • Mihir Bellare, Chanathip Namprempre, 2007, Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm

    Variable is_plaintext : val.
    Variable is_ciphertext : val.
    Variable is_key : val.

    Definition CCA : val :=
      λ:"b" "adv" "scheme" "Qenckey" "Qencgen" "Qdec" "Qdecgen",
        let: "enc_scheme" := get_enc_scheme "scheme" #() in
        let: "key" := get_keygen "scheme" #() in
        let: "enc_gen" := get_enc "enc_scheme" in
        let: "dec_gen" := get_dec "enc_scheme" in
        let: "enc_key" := λ: "msg", (get_enc "enc_scheme") "key" "msg" in
        let: "dec_key" := λ: "msg", (get_dec "enc_scheme") "key" "msg" in
        let: "enc_lr" := λ: "msgs",
          "enc_key" (if: "b" then (Fst "msgs") else (Snd "msgs")) in
        let: "oracle_lr" :=
          q_calls_general_test
          (λ: "p", is_plaintext (Fst "p") `and` is_plaintext (Snd "p"))
          "Qenckey" "enc_lr" in
      let: "oracle_lr" := λ: "msg1" "msg2", "oracle_lr" ("msg1", "msg2") in
      let: "oracle_enc_gen" :=
        q_calls_general_test
          (λ: "p", is_key (Fst "p") `and` is_plaintext (Snd "p"))
          "Qencgen"
          (λ: "p", "enc_gen" (Fst "p") (Snd "p")) in
      let: "oracle_enc_gen" := λ: "k" "msg", "oracle_enc_gen" ("k", "msg") in
      let: "oracle_dec_gen" :=
        q_calls_general_test
          (λ: "p", is_key (Fst "p") `and` is_ciphertext (Snd "p"))
          "Qdecgen"
          (λ: "p", "dec_gen" (Fst "p") (Snd "p")) in
      let: "oracle_dec_gen" := λ: "k" "msg", "oracle_dec_gen" ("k", "msg") in
        let: "oracle_dec" :=
          q_calls_general_test is_ciphertext "Qdec" "dec_key" in
        let: "b'" := "adv" "oracle_enc_gen" "oracle_lr" "oracle_dec" "oracle_dec_gen" in
        "b'".

  End CCA.

Section INT_PTXT.

Integrity of plaintexts game for symmetric encryption References:
  • Daniel Jost, 2018, Christian Badertscher, Fabio Banfi, A note on the equivalence of IND-CCA & INT-PTXT and IND-CCA & INT-CTXT
  • Nicolas Klose, 2021, Characterizing Notions For Secure Cryptographic Channels
  • Mihir Bellare, Chanathip Namprempre, 2007, Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm

  Variable is_plaintext : val.
  Variable is_ciphertext : val.

  Variable elem_eq : val.

  Definition PTXT : val :=
    λ: "b" "adv" "scheme" "Q_enc" "Q_dec" "Q_lr",
      let: "record_plaintext" := init_linked_list #() in
      let: "enc_scheme" := get_enc_scheme "scheme" #() in
      let: "enc" := get_enc "enc_scheme" in
      let: "dec" := get_dec "enc_scheme" in
      let: "key" := get_keygen "scheme" #() in
      let: "enc_key" := λ: "msg", add_list "record_plaintext" "msg";;
        "enc" "key" "msg" in
      let: "dec_key" := λ: "msg", "dec" "key" "msg" in
      let: "rr_key_b" :=
        if: "b" then
          λ: "c",
          let: "decrypted'" := "dec" "key" "c" in
          elem_of_linked_list elem_eq "record_plaintext" "decrypted'"
        else
          λ: <>, #true in
      let: "oracle_enc" := q_calls_general_test is_plaintext "Q_enc" "enc_key" in
      let: "oracle_dec" := q_calls_general_test_eager is_ciphertext "Q_dec" "dec_key" in
      let: "oracle_lr" := q_calls_general_test is_ciphertext "Q_lr" "rr_key_b" in
      let: "b'" := "adv" "oracle_enc" "oracle_dec" "oracle_lr" in
      "b'".

  Context `{!approxisRGS Σ}.

  Section lrel_types_defs.

  Variable lrel_msg : lrel Σ.
  Variable lrel_cipher : lrel Σ.

  Definition lrel_enc_oracle : lrel Σ :=
    lrel_msg → (() + lrel_cipher).

  Definition lrel_dec_oracle : lrel Σ :=
    lrel_cipher → (() + lrel_msg).

  Definition lrel_oracle_lr : lrel Σ :=
    lrel_cipher → (() + lrel_bool).

  Definition lrel_adv : lrel Σ :=
    lrel_enc_oracle → lrel_dec_oracle → lrel_oracle_lr → lrel_bool.

  End lrel_types_defs.

End INT_PTXT.