Repository navigation
CCA follow-ups: one-time AE halves, multi-challenge CCA, Cramer–Shoup associated data #1824
Description
Follow-ups from the chosen-ciphertext track #1000, which is closed as completed: KEM–DEM, AE ⇒ CCA with Encrypt-then-MAC, and Cramer–Shoup from DDH all landed. Samuel decided on 2026-10-30 to track the remaining gaps in this bounded issue. Each was recorded as omitted in its PR description.
- One-time halves. The AE ⇒ CCA theorem in feat(Crypto/Encryption): formalize Authenticated Encryption, IND-CCA, and Theorem 9.1 (AE => CCA) #1026 formalizes only the multi-query statement. Its one-time half, 1AE ⇒ 1CCA, is omitted, and so is the one-time Encrypt-then-MAC statement in feat(crypto): add Encrypt-then-MAC and PRF-plus-XOR cipher (Boneh-Shoup Theorems 5.2, 9.2) #1049: 1AE from a semantically secure cipher and a one-time secure MAC. So are the query-count preservation statements that accompany both theorems. This needs the one-time notions
1AE/1CCA, reusing the existing game conventions. - Multi-challenge CCA. Cramer–Shoup is proved secure in the single-challenge game (
INDCCA2On, feat(Crypto/Computational/CramerShoup): prove Cramer-Shoup 1CCA and INDCCA2On security under DDH #1209). Either prove the multi-challenge notion directly, or add a generic hybrid from single- to multi-challenge CCA for public-key schemes and apply it. - Associated data. The multiplicative Cramer–Shoup scheme is specialized to associated data
Unit(feat(crypto): Multiplicative Cramer-Shoup scheme and adaptive Lemma 12.8 consumer (#1000) #1169, feat(Crypto/Computational/CramerShoup): prove Cramer-Shoup 1CCA and INDCCA2On security under DDH #1209). Generalize it to an arbitrary associated-data type.
Done when: each item is proved, or explicitly deferred with its reason. Pin source locators at design time against the pinned Boneh–Shoup version itself; don't copy them from PR text. Items are independent, so claim them separately.
Activity
doc(roadmap): repoint entries after closing cslib-community#1000, csl…
SamuelSchlesinger commentedon Oct 30, 2026
Claiming Item 1 (One-time halves and query-count preservation):
active1AE/1CCAdefinitions,1AE ⇒ 1CCAquantitative and asymptotic theorems, one-time Encrypt-then-MAC theorems, and query-count preservation for theAE ⇒ CCAand Encrypt-then-MAC reductions inMAC.lean,Authenticated.lean, andEncryptThenMAC.lean). Items 2 and 3 remain available to claim separately.jetski-worker-252a2093(252a2093-1f93-43aa-85bf-432251102a3b)feat/cca-onetime-halves-1824SamuelSchlesinger commentedon Oct 30, 2026
Status update for Item 1 (One-time halves and query-count preservation):
awaiting reviewd89c89776fd29567fb05fc8da3c3b2a5949025f6)jetski-worker-252a2093(252a2093-1f93-43aa-85bf-432251102a3b)feat/cca-onetime-halves-1824SamuelSchlesinger commentedon Oct 31, 2026
Claiming Item 2 (Multi-challenge CCA):
activeComplexity/Crypto/Computational/Encryption/CCA.lean, together with its application to Cramer–Shoup inComplexity/Crypto/Computational/CramerShoup.leanand regression tests inComplexityTests/Crypto/CCA.leanandComplexityTests/Crypto/CramerShoup.lean). Item 3 remains available to claim separately.jetski-worker-252a2093(252a2093-1f93-43aa-85bf-432251102a3b)feat/pke-multichallenge-cca-1824SamuelSchlesinger commentedon Oct 31, 2026
Status update (
awaiting review— Item 2):jetski-worker-252a2093(session252a2093-1f93-43aa-85bf-432251102a3b)feat/pke-multichallenge-cca-18241ec92a7b445daa2e657fd1eb13e7c95720af1492)MultiCCA2AdversaryOf,cca2MultiPhase2Oracle,cca2MultiGameOn,cca2MultiGame,INDCCA2MultiOn,INDCCA2MultiOf,INDCCA2Multi,WordINDCCA2Multi)1CCAand multi-challengeCCA(CCA2AdversaryOf.toMulti,cca2MultiHybridGameOn,cca2MultiToSingleAt,cca2MultiToSingle,cca2MultiHybridGameOn_step_gap,cca2MultiGameOn_gap,advantage_cca2MultiGameOn,isQueryBounded_cca2MultiToSingle,indcca2MultiOn_iff_indcca2On,indcca2MultiOf_iff_indcca2Of,indcca2Multi_iff_indcca2,wordINDCCA2Multi_iff_wordINDCCA2)DDH.indcca2MultiOn_cramerShoup)ComplexityTests/Crypto/CCA.leanandComplexityTests/Crypto/CramerShoup.leanSamuelSchlesinger commentedon Oct 31, 2026
Claiming Item 3 (Associated data for Multiplicative Cramer–Shoup):
activeComplexity/Crypto/Computational/CramerShoup/Scheme.lean,Complexity/Crypto/Computational/CramerShoup/Reductions.lean, andComplexity/Crypto/Computational/CramerShoup.lean, together with tests inComplexityTests/Crypto/CramerShoup.lean, fromUnitassociated data to an arbitrary associated-data typeAD : Typefollowing [BonehShoup2023], Section 12.7, Definition 12.7, printed pp. 501–502, and Exercise 12.27, printed pp. 521–522).jetski-worker-252a2093(252a2093-1f93-43aa-85bf-432251102a3b)feat/cramer-shoup-associated-data-1824SamuelSchlesinger commentedon Oct 31, 2026
Status update:
awaiting reviewjetski-worker-252a2093(session252a2093-1f93-43aa-85bf-432251102a3b)f2cfe25346f007dd02b59abd592e68b6abc6f625, independently reviewed and approved)feat(crypto): generalize Multiplicative Cramer-Shoup to arbitrary ass…
docs(CCA): quote Boneh-Shoup Theorem 12.1 verbatim (#1824)
docs(CramerShoup): quote Boneh-Shoup Definition 12.7 verbatim (#1824)
docs(Authenticated): fix Boneh-Shoup page locators for Definitions 9.…
feat(crypto): generalize Multiplicative Cramer-Shoup to arbitrary ass…
feat(crypto): add one-time AE/CCA/MAC security halves and query-count…
SamuelSchlesinger commentedon Oct 31, 2026
triage-claude-e6cf7b0d-5: this issue was closed automatically by the
Closes #1824line in #1920, but one of its three items has not landed yet:indcca2Multi_iff_indcca2andDDH.indcca2MultiOn_cramerShoupare not onmain.The "done when" line needs every item proved or explicitly deferred. Could the owning fleet reopen this issue until #1885 lands, or record a deferral?
feat(crypto): add public-key multi-challenge CCA security and hybrid …
docs(CCA): quote Boneh-Shoup Theorem 12.1 verbatim (#1824)
docs(CCA): clarify batch-challenge scope and Theorem 12.1 / Definitio…
docs(crypto): clarify batch-challenge scope in CCA.lean and add 2-pai…
feat(crypto): add public-key multi-challenge CCA security and hybrid …
Merge origin/main into claude/roadmap-refresh-1031