3.3. CKA from KEM🔗

Definition3.3.1

Group: CKA from KEM. (2)

Group member previews

Preview

Theorem 3.3.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 3.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

def scheme {m : Type → Type u} [Monad m] {K PK SK C : Type}
    (kem : KEMScheme m K PK SK C)
    (hDet : DeterministicDecaps kem)
    (leak : RandLeak kem) :
    CKAScheme m (InitKey PK SK) (State PK SK) K (Message C PK) leak.Rand where
  initKeyGen := kem.keygen
  initA := fun ik => return initA ik
  initB := fun ik => return initB ik
  sendA := send kem
  sendArleak := sendRleak kem leak
  recvA := recv hDet
  sendB := send kem
  sendBrleak := sendRleak kem leak
  recvB := recv hDet

uses Definition 3.1.1 · github #3

Lean code for Definition3.3.1●1 definition

defdefined in SecureMessaging/CKA/FromKEM/Construction.lean

complete

def kemCKA.scheme.{u} {m : Type → Type u} [Monad m] {K PK SK C : Type}
  (kem : KEMScheme m K PK SK C) (hDet : kem.DeterministicDecaps)
  (leak : kem.RandLeak) :
  CKAScheme m (kemCKA.InitKey PK SK) (kemCKA.State PK SK) K
    (kemCKA.Message C PK) leak.Rand

def kemCKA.scheme.{u} {m : Type → Type u}
  [Monad m] {K PK SK C : Type}
  (kem : KEMScheme m K PK SK C)
  (hDet : kem.DeterministicDecaps)
  (leak : kem.RandLeak) :
  CKAScheme m (kemCKA.InitKey PK SK)
    (kemCKA.State PK SK) K
    (kemCKA.Message C PK) leak.Rand

Generic CKA scheme induced by a KEM.

The type parameters specialize the abstract CKA interface as follows:

* `IK = PK × SK`, the initial KEM key pair;
* `St = kemCKA.State PK SK`, a phase-tagged public/secret key state;
* `I = K`, the KEM shared key used as the CKA epoch key;
* `Rho = C × PK`, the protocol-message space;
* `Rand = RandLeak.Rand leak`, the encapsulation and key-generation
  randomness leaked by one send.

The send and receive algorithms are the same for A and B; only initialization
differs, with A starting from the public key and B from the secret key. For a
KEM that does not expose its coins, instantiate `leak` with the trivial
package `RandLeak.noLeak kem`.

Theorem3.3.2

Group: CKA from KEM. (2)

Group member previews

Preview

Definition 3.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

\todo

theorem correctness [DecidableEq K]
    (kem : KEMScheme ProbComp K PK SK C)
    (hDet : DeterministicDecaps kem)
    (leak : RandLeak kem)
    (hkem : kem.PerfectlyCorrect ProbCompRuntime.probComp)
    (adv : CKAScheme.CKACorrectnessAdversary (Message C PK) K) :
    Pr[= true | CKAScheme.correctnessExp (scheme kem hDet leak) adv] = 1

uses Definition 3.3.1 · Definition 3.1.3 · github #4

Lean code for Theorem3.3.2●1 theorem

theoremdefined in SecureMessaging/CKA/FromKEM/Correctness.lean

complete

theorem kemCKA.correctness {K PK SK C : Type} [DecidableEq K]
  (kem : KEMScheme ProbComp K PK SK C) (hDet : kem.DeterministicDecaps)
  (leak : kem.RandLeak)
  (hkem : kem.PerfectlyCorrect ProbCompRuntime.probComp)
  (adv : CKAScheme.CKACorrectnessAdversary (kemCKA.Message C PK) K) :
  Pr[= true | (kemCKA.scheme kem hDet leak).correctnessExp adv] = 1

theorem kemCKA.correctness {K PK SK C : Type}
  [DecidableEq K]
  (kem : KEMScheme ProbComp K PK SK C)
  (hDet : kem.DeterministicDecaps)
  (leak : kem.RandLeak)
  (hkem :
    kem.PerfectlyCorrect
      ProbCompRuntime.probComp)
  (adv :
    CKAScheme.CKACorrectnessAdversary
      (kemCKA.Message C PK) K) :
  Pr[= true |
      (kemCKA.scheme kem hDet
            leak).correctnessExp
        adv] =
    1

Correctness of the CKA-from-KEM construction in the existing CKA correctness
game.

For every adversary using only the honest send/receive oracles, the game returns
`true` with probability one under the KEM correctness hypothesis. The statement
is proved for an arbitrary randomness-leak package `leak`: the correctness game
never queries the randomness-leaking send oracles, so correctness is independent
of the choice of `leak`.

Theorem3.3.3

Group: CKA from KEM. (2)

Group member previews

Preview

Definition 3.3.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

\todo

theorem security [SampleableType K] [DecidableEq K]
    (kem : KEMScheme ProbComp K PK SK C)
    (hDet : DeterministicDecaps kem)
    (hkem : kem.PerfectlyCorrect ProbCompRuntime.probComp)
    (leak : RandLeak kem)
    (adv : Adversary (kem := kem) leak)
    (gp : CKAScheme.GameParams)
    (hgp : AdmissibleParams gp) :
    CKAScheme.ckaDistAdvantage (scheme kem hDet leak) adv gp ≤
      KEMScheme.IND_CPA_Advantage (kem := kem) ProbCompRuntime.probComp
        (ckaToINDCPAReduction kem hDet leak adv gp)

uses Definition 3.3.1 · Definition 3.1.4 · github #5

Lean code for Theorem3.3.3●1 theorem

theoremdefined in SecureMessaging/CKA/FromKEM/Security.lean

complete

theorem kemCKA.security {K PK SK C : Type} [SampleableType K] [DecidableEq K]
  (kem : KEMScheme ProbComp K PK SK C) (hDet : kem.DeterministicDecaps)
  (hkem : kem.PerfectlyCorrect ProbCompRuntime.probComp)
  (leak : kem.RandLeak) (adv : kemCKA.Adversary leak)
  (gp : CKAScheme.GameParams) (hgp : kemCKA.AdmissibleParams gp) :
  (kemCKA.scheme kem hDet leak).ckaDistAdvantage adv gp ≤
    KEMScheme.IND_CPA_Advantage ProbCompRuntime.probComp
      (kemCKA.ckaToINDCPAReduction kem hDet leak adv gp)

theorem kemCKA.security {K PK SK C : Type}
  [SampleableType K] [DecidableEq K]
  (kem : KEMScheme ProbComp K PK SK C)
  (hDet : kem.DeterministicDecaps)
  (hkem :
    kem.PerfectlyCorrect
      ProbCompRuntime.probComp)
  (leak : kem.RandLeak)
  (adv : kemCKA.Adversary leak)
  (gp : CKAScheme.GameParams)
  (hgp : kemCKA.AdmissibleParams gp) :
  (kemCKA.scheme kem hDet
          leak).ckaDistAdvantage
      adv gp ≤
    KEMScheme.IND_CPA_Advantage
      ProbCompRuntime.probComp
      (kemCKA.ckaToINDCPAReduction kem
        hDet leak adv gp)

Security reduction for CKA from a KEM.

For every perfectly correct KEM, CKA adversary, and admissible challenge
parameters, the IND-CPA advantage of the concrete reduction
`ckaToINDCPAReduction kem hDet leak adv gp` upper-bounds the CKA distinguishing
advantage of the constructed protocol — in fact the two advantages are equal,
so the stated bound holds with equality.

The bound compares like with like: `CKAScheme.ckaDistAdvantage` is the gap
between the real-key and random-key branches of the CKA game (twice
`CKAScheme.ckaGuessAdvantage`), and `KEMScheme.IND_CPA_Advantage` is the
Boolean bias `|Pr[true] - Pr[false]|` of the single IND-CPA game.

N.B. ACD19's sampled-bit guessing advantage is half of `ckaDistAdvantage`
(`CKAScheme.ckaGuessAdvantage_eq_ckaDistAdvantage_div_two`); the paper's no-leak
construction is the instance `RandLeak.noLeak kem`.

References:

Alwen et al. (2019)