論文の概要: Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

• arxiv url: http://arxiv.org/abs/2604.24670v2
• Date: Tue, 28 Apr 2026 17:48:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-29 14:06:43.851063
• Title: Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware
• Title（参考訳）: マスケバレットリダクションのためのマシーンシェッケード心電図:ポスト量子暗号ハードウェアにおける1ビットサイドチャネル漏れバリア
• Authors: Ray Iskander, Khaled Kirah,
• Abstract要約: バレットリダクションはNTTベースのポスト量子暗号実装のすべての非線形コアである。 既存の構成フレームワークはGF(2)上のマスキングに対処している。 PF-PINIはPF-PINI(2)を満たす。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Barrett reduction is the nonlinear core of every practical NTT-based post-quantum cryptography implementation. Existing composition frameworks (ISW, t-SNI, PINI, DOM) address Boolean masking over GF(2); none provides a machine-checked characterization of Barrett's leakage under first-order arithmetic masking and the first-order probing model over prime fields. Building on our prior series, QANARY [15], partial-NTT-masking margins [14], algebraic foundations [16], and butterfly composition [18], we close this gap. We prove a trichotomy: for any $q > 0$ and shift $s$, the Barrett internal wire map $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ has preimage cardinality in $\{0, 1, 2\}$, never more. We call this the 1-Bit Barrier: max-multiplicity 2 implies at most 1 bit of min-entropy loss per internal wire, universal over all moduli. The count-zero cases, unreachable output values, reveal that actual leakage is often strictly less than 1 bit, making the bound conservative. We introduce PF-PINI (Prime-Field PINI): Barrett satisfies PF-PINI(2); the Cooley-Tukey butterfly satisfies PF-PINI(1). We observe (not yet proved) that with fresh inter-stage masking, the composed pipeline has max-multiplicity $\max(k_1, k_2)$, so the 1-Bit Barrier propagates. The trichotomy, the PF-PINI instantiations, and cardinality results are machine-checked in Lean 4 with Mathlib: 12 proved results, zero sorry, universal over all $q > 0$ (the min-entropy bound follows by standard definitions). Adams Bridge lacks fresh inter-stage masking, violating PF-PINI composition and explaining why Papers 1 [15] and 2 [14] found vulnerabilities. NIST IR 8547 recommends formal methods for PQC implementation validation. The 1-Bit Barrier provides the first universal machine-checked cardinality bound for masked Barrett reduction in ML-KEM (FIPS 203) and ML-DSA (FIPS 204), with a corresponding 1-bit leakage interpretation.
• Abstract（参考訳）: バレットリダクションはNTTベースのポスト量子暗号実装のすべての非線形コアである。 既存の合成フレームワーク (ISW, t-SNI, PINI, DOM) は GF(2) 上のブールマスキング(Boolean masking)に対処するが、一階算術マスキングの下でのバレットの漏洩のマシンチェックと素体上の一階探索モデルを提供するものはない。 QANary [15], partial-NTT-masking margins [14], algebraic foundations [16], butterfly composition [18], we close this gap。 任意の$q > 0$ に対して、シフト $s$ に対して、バレットの内部ワイヤマップ $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ は $\{0, 1, 2\}$ の事前濃度を持つ。 最大乗算性 2 は、すべてのモジュライ上で普遍的に、内部線当たりの最小エントロピー損失の少なくとも1ビットを暗示する。 カウントゼロの場合、到達不能な出力値により、実際のリークは1ビット未満で、境界が保守的であることがしばしば明らかになる。 本稿では,PF-PINI(Prime-Field PINI)を紹介する。Barrett は PF-PINI(2),Colley-Tukey butterfly は PF-PINI(1) を満たす。 我々は、新しいステージ間マスキングでは、合成パイプラインは最大多重度$\max(k_1, k_2)$を持つので、1ビットバリアは伝播する(まだ証明されていない)。 三分法、PF-PINIのインスタンス化、および濃度結果は、Lean 4においてMathlibで機械チェックされる: 12の証明結果、ゼロの謝罪、すべての$q > 0$の普遍性(ミンエントロピー境界は標準定義によって従う)。 Adams Bridgeには、新しいステージ間マスキング、PF-PINIの構成違反、Paper 1 [15]と2 [14]が脆弱性を発見した理由の説明が欠けている。 NIST IR 8547は、PQCの実装検証のための正式なメソッドを推奨している。 1ビットバリアは、ML-KEM (FIPS 203) と ML-DSA (FIPS 204) におけるマスク付きバレット還元のための最初の普遍的なマシンチェックされた基数であり、対応する1ビットリーク解釈を持つ。

関連論文リスト

• Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware [0.0]
  量子後暗号(PQC)アクセラレーターは、$mathbbZ_q$を超えるパイプライン化された数理論変換ステージに依存している。 我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。 マシンでチェックした3つの結果は、Lean 4でMathlibとともに紹介します。
  論文  参考訳（メタデータ） (2026-04-22T17:19:22Z)
• From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification [0.0]
  ポスト量子暗号(PQC)ハードウェアにおけるマスキングの形式的検証は、有限領域上のSMTソルバに依存する。 我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。 構造依存分析フレームワークであるQANaryは、Adams Bridge ML-DSA/ML-KEMアクセラレーターの30モジュールにわたる117万の細胞を検証した。
  論文  参考訳（メタデータ） (2026-04-20T18:17:22Z)
• Fair Decoder Baselines and Rigorous Finite-Size Scaling for Bivariate Bicycle Codes on the Quantum Erasure Channel [0.14323566945483496]
  BB符号のBP-OSDデコードと並行して,非インフォームおよびエンフェラジャー対応のサーフェスコードベースラインを動作させる。 標準偏極重みMWPMと消去情報がないため、消去チャネル上でのランダムな推測と性能は一致しない。 BB at $N=1296$は、表面符号の2倍の閾値で、12$times$より低い正規化オーバーヘッドを持つ。
  論文  参考訳（メタデータ） (2026-03-19T15:53:51Z)
• Hardness of High-Dimensional Linear Classification [58.29089693778071]
  我々は、最大半空間離散性問題に対する次元下界の新たな指数関数を確立する。 どちらも計算幾何学と機械学習の基本的問題であり、その正確で近似的な形式である。
  論文  参考訳（メタデータ） (2026-03-19T15:53:41Z)
• A lower bound on the space overhead of fault-tolerant quantum computation [51.723084600243716]
  しきい値定理は、フォールトトレラント量子計算の理論における基本的な結果である。 振幅雑音を伴う耐故障性量子計算の最大長に対する指数的上限を証明した。
  論文  参考訳（メタデータ） (2022-01-31T22:19:49Z)
• 1$\times$N Block Pattern for Network Sparsity [90.43191747596491]
  我々は,この制限を破るために,ブロック間隔パターン(ブロックプルーニング)を1時間で定義する新しい概念を提案する。 このパターンはMobileNet-V2の上位1の精度でフィルタプルーニングよりも約3.0%改善されている。 また、重み付けによるCortex-A7 CPUの56.04msの推論も得る。
  論文  参考訳（メタデータ） (2021-05-31T05:50:33Z)
• BRST-BV Quantum Actions for Constrained Totally-Symmetric Integer HS Fields [77.34726150561087]
  非最小制約BRST-BVラグランジアン定式化は、$d$次元ミンコフスキー空間における完全対称な質量を持たないHS場に対して提示される。 フォック空間量子作用は、全BRST-BV作用におけるゲージ固定フェルミオン$Psi$の変分微分により、全一般化場-反場ベクトルのシフトとして構成される。
  論文  参考訳（メタデータ） (2020-10-29T16:40:32Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。