Message Authentication Codes

This file defines keyed message-authentication-code algorithms together with their standard UF-CMA security game.

structure MacAlg (m : Type → Type v) [Monad m] (M K T : Type) : Type v

MAC algorithm with computations in the monad m, where M is the message space, K the key space, and T the tag space.

• keygen : m K
• tag : K → M → m T
• verify : K → M → T → m Bool

def MacAlg.taggingOracle {m : Type → Type v} [Monad m] {M K T : Type} (macAlg : MacAlg m M K T) (k : K) : QueryImpl (OracleSpec.ofFn fun (x : M) => T) (WriterT (OracleSpec.ofFn fun (x : M) => T).QueryLog m)

Oracle exposing chosen-message tagging queries while logging every queried message.

def MacAlg.PerfectlyComplete {m : Type → Type v} [Monad m] {M K T : Type} (macAlg : MacAlg m M K T) (runtime : ProbCompRuntime m) : Prop

Perfect completeness for a MAC: honestly generated tags always verify.

structure MacAlg.UF_CMA_Adversary {ι : Type u} {spec : OracleSpec ι} {M K T : Type} (_macAlg : MacAlg (OracleComp spec) M K T) : Type u

UF-CMA adversary for a MAC: it receives oracle access to the tagging oracle and outputs a candidate forgery (msg, tag).

• main : OracleComp (spec + OracleSpec.ofFn fun (x : M) => T) (M × T)

def MacAlg.UF_CMA_Exp {ι : Type u} {spec : OracleSpec ι} {M K T : Type} [DecidableEq M] [DecidableEq T] {macAlg : MacAlg (OracleComp spec) M K T} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : macAlg.UF_CMA_Adversary) : SPMF Bool

UF-CMA experiment for a MAC: the adversary succeeds iff it outputs a valid tag for a fresh message under the challenge key.

noncomputable def MacAlg.UF_CMA_Advantage {ι : Type u} {spec : OracleSpec ι} {M K T : Type} [DecidableEq M] [DecidableEq T] {macAlg : MacAlg (OracleComp spec) M K T} (runtime : ProbCompRuntime (OracleComp spec)) (adversary : macAlg.UF_CMA_Adversary) : ENNReal

UF-CMA advantage for a MAC, represented as the probability of producing a valid forgery on a fresh message.