Auth.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 98 of 353 lines trusted trust banner B3, trusted in part source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Declarations on this page (21)

SPQR V1: Authenticator (spqr/src/authenticator.rs, src/authenticator/serialize.rs)

Trusted in part. The theorems of Computational/Theorems/ use every definition in this file except compare_prefix, Authenticator.verifyCt_prefix, Authenticator.verifyHdr_prefix and the test vectors in Tests, which are checked by Lean (see Computational/docs/TRUSTED_BASE.md).

Models SPQR's epoch authenticator (Mac, AuthError, Authenticator with macSize, new, update, intoPb, fromPb), panic-explicit HMAC-SHA256 tag computation and constant-time verification (macCt, verifyCt, verifyCtError, macHdr, verifyHdr, verifyHdrError, hmacU32UnwrapPanic), and unchecked helpers (macCtUnchecked, macHdrUnchecked, verifyCt_eq_ok_prefix, verifyHdr_eq_ok_prefix).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.HMAC

4 declarations not shown (lines 39–61): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.compare_prefix, CryptoVerification.LibsignalSpqrV1.compare_eq_ok_prefix, CryptoVerification.LibsignalSpqrV1.length_sha256With, CryptoVerification.LibsignalSpqrV1.length_hmacWith

Types and constants (spqr/src/authenticator.rs)

abbrev MacL65 ↗#

abbrev Mac := Bytes

abbrev hmacU32UnwrapPanicL67–70 ↗#

Panic site in libcrux-hmac 0.0.8 (src/impl_hacl.rs:12,14): u32 length unwrap when key.length ≥ 2^32 or data.length ≥ 2^32.

abbrev hmacU32UnwrapPanic : SpqrPanic :=
  .site "libcrux-hmac impl_hacl.rs:12/14 u32 unwrap"

inductive AuthErrorL72–80 ↗#

spqr::authenticator::Error (src/authenticator.rs:11–24).

inductive AuthError where
  | invalidCtMac
  | invalidHdrMac
  | authenticatorRootKeyPresent
  | authenticatorRootKeyMissing
  | authenticatorMacKeyPresent
  | authenticatorMacKeyMissing
  deriving DecidableEq, Repr, Inhabited

def AuthError.toErrorL82–83 ↗#

impl From<authenticator::Error> for Error (src/lib.rs:144–147).

def AuthError.toError : AuthError → Error := fun _ => .macVerifyFailed

structure AuthenticatorL85–89 ↗#

spqr::authenticator::Authenticator (src/authenticator.rs:27–30).

structure Authenticator where
  rootKey : Mac
  macKey : Mac
  deriving DecidableEq, Repr, Inhabited

namespace Authenticator

abbrev macSizeL93 ↗#

abbrev macSize : ℕ := 32

def updateLabelL95–96 ↗#

def updateLabel : Bytes :=
  "Signal_PQCKA_V1_MLKEM768:Authenticator Update".toList.map fun c => BitVec.ofNat 8 c.toNat

def ctLabelL98–99 ↗#

def ctLabel : Bytes :=
  "Signal_PQCKA_V1_MLKEM768:ciphertext".toList.map fun c => BitVec.ofNat 8 c.toNat

def hdrLabelL101–102 ↗#

def hdrLabel : Bytes :=
  "Signal_PQCKA_V1_MLKEM768:ekheader".toList.map fun c => BitVec.ofNat 8 c.toNat

def updateL104–112 ↗#

Authenticator::update (src/authenticator.rs:44–54): derives (rootKey, macKey) via 64-byte HKDF-SHA256 from rootKey ++ k and updateLabel ++ ep.to_be_bytes() under a 32-byte zero salt.

def update (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (k : Bytes) : Authenticator :=
  let ikm := self.rootKey ++ k
  let info := updateLabel ++ toBEBytes 8 ep
  let kdfOut := hkdfToVecUnchecked F (List.replicate 32 0) ikm info 64
  { rootKey := kdfOut.take 32
    macKey := kdfOut.drop 32 }

def newL114–117 ↗#

Authenticator::new (src/authenticator.rs:35–42).

def new (F : ShaState → List (BitVec 8) → ShaState) (rootKey : Bytes) (ep : Epoch) : Authenticator :=
  let result : Authenticator := { rootKey := List.replicate 32 0, macKey := List.replicate 32 0 }
  result.update F ep rootKey

def macCtUncheckedL119–122 ↗#

def macCtUnchecked (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (ct : Bytes) : Mac :=
  let ctMacData := ctLabel ++ toBEBytes 8 ep ++ ct
  (hmacWith F self.macKey ctMacData).take macSize

1 declaration not shown (lines 124–128): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.length_macCtUnchecked

def macCtL130–139 ↗#

Authenticator::mac_ct (src/authenticator.rs:66–79): HMAC-SHA256 tag over ctLabel ++ ep.to_be_bytes() ++ ct, panicking with hmacU32UnwrapPanic if key or input length reaches 2^32.

def macCt (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (ct : Bytes) : Except SpqrPanic Mac :=
  let ctMacData := ctLabel ++ toBEBytes 8 ep ++ ct
  if self.macKey.length < 2 ^ 32 ∧ ctMacData.length < 2 ^ 32 then
    .ok (self.macCtUnchecked F ep ct)
  else
    .error hmacU32UnwrapPanic

2 declarations not shown (lines 141–153): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.macCt_of_lt, CryptoVerification.LibsignalSpqrV1.Authenticator.verifyCt_prefix

def verifyCtL155–163 ↗#

Authenticator::verify_ct (src/authenticator.rs:57–63): checks expectedMac against macCt F ep ct via Core.compare (which compares 0..expectedMac.length and panics if expectedMac.length > 32).

def verifyCt (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (ct expectedMac : Bytes) :
      Except SpqrPanic (Except AuthError Unit) := do
  let mac ← self.macCt F ep ct
  let c ← compare expectedMac mac
  return if c != 0#8 then .error .invalidCtMac else .ok ()

def verifyCtErrorL165–168 ↗#

def verifyCtError (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (ct expectedMac : Bytes) :
      Except SpqrPanic (Except Error Unit) :=
  (self.verifyCt F ep ct expectedMac).map (Except.mapError AuthError.toError)

1 declaration not shown (lines 170–179): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.verifyCt_eq_ok_prefix

def macHdrUncheckedL181–184 ↗#

def macHdrUnchecked (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (hdr : Bytes) : Mac :=
  let ctMacData := hdrLabel ++ toBEBytes 8 ep ++ hdr
  (hmacWith F self.macKey ctMacData).take macSize

1 declaration not shown (lines 186–190): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.length_macHdrUnchecked

def macHdrL192–201 ↗#

Authenticator::mac_hdr (src/authenticator.rs:91–104): HMAC-SHA256 tag over hdrLabel ++ ep.to_be_bytes() ++ hdr, panicking with hmacU32UnwrapPanic if key or input length reaches 2^32.

def macHdr (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (hdr : Bytes) : Except SpqrPanic Mac :=
  let ctMacData := hdrLabel ++ toBEBytes 8 ep ++ hdr
  if self.macKey.length < 2 ^ 32 ∧ ctMacData.length < 2 ^ 32 then
    .ok (self.macHdrUnchecked F ep hdr)
  else
    .error hmacU32UnwrapPanic

2 declarations not shown (lines 203–215): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.macHdr_of_lt, CryptoVerification.LibsignalSpqrV1.Authenticator.verifyHdr_prefix

def verifyHdrL217–224 ↗#

Authenticator::verify_hdr (src/authenticator.rs:82–88): checks expectedMac against macHdr F ep hdr via Core.compare (panicking if expectedMac.length > 32).

def verifyHdr (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (hdr expectedMac : Bytes) :
      Except SpqrPanic (Except AuthError Unit) := do
  let mac ← self.macHdr F ep hdr
  let c ← compare expectedMac mac
  return if c != 0#8 then .error .invalidHdrMac else .ok ()

def verifyHdrErrorL226–229 ↗#

def verifyHdrError (F : ShaState → List (BitVec 8) → ShaState)
    (self : Authenticator) (ep : Epoch) (hdr expectedMac : Bytes) :
      Except SpqrPanic (Except Error Unit) :=
  (self.verifyHdr F ep hdr expectedMac).map (Except.mapError AuthError.toError)

1 declaration not shown (lines 231–240): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.verifyHdr_eq_ok_prefix

def intoPbL242–243 ↗#

def intoPb (self : Authenticator) : ProtoAuthenticator :=
  { rootKey := self.rootKey, macKey := self.macKey }

def fromPbL245–246 ↗#

def fromPb (pb : ProtoAuthenticator) : Authenticator :=
  { rootKey := pb.rootKey, macKey := pb.macKey }

2 declarations not shown (lines 248–252): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Authenticator.fromPb_intoPb, CryptoVerification.LibsignalSpqrV1.Authenticator.intoPb_fromPb

end Authenticator

11 declarations not shown (lines 262–349): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.Tests.asciiBytes, CryptoVerification.LibsignalSpqrV1.Tests.auth1, CryptoVerification.LibsignalSpqrV1.Tests.auth1Expected, CryptoVerification.LibsignalSpqrV1.Tests.auth1_eq, CryptoVerification.LibsignalSpqrV1.Tests.auth1_macCt, CryptoVerification.LibsignalSpqrV1.Tests.auth1_macHdr, CryptoVerification.LibsignalSpqrV1.Tests.v0Auth0, CryptoVerification.LibsignalSpqrV1.Tests.v0Auth0Expected, CryptoVerification.LibsignalSpqrV1.Tests.v0_update_vec0, CryptoVerification.LibsignalSpqrV1.Tests.v0Auth1, CryptoVerification.LibsignalSpqrV1.Tests.v0Auth1Expected

end CryptoVerification.LibsignalSpqrV1