論文の概要: From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

• arxiv url: http://arxiv.org/abs/2604.18717v2
• Date: Wed, 22 Apr 2026 17:58:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-23 15:36:10.446188
• Title: From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification
• Title（参考訳）: 有限列挙から普遍証明へ:PQCハードウェアマスキング検証のためのリング理論の基礎
• Authors: Ray Iskander, Khaled Kirah,
• Abstract要約: ポスト量子暗号(PQC)ハードウェアにおけるマスキングの形式的検証は、有限領域上のSMTソルバに依存する。 我々の以前の研究は大規模な構造依存解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した。 構造依存分析フレームワークであるQANaryは、Adams Bridge ML-DSA/ML-KEMアクセラレーターの30モジュールにわたる117万の細胞を検証した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification of masking in post-quantum cryptographic (PQC) hardware relies on SMT solvers over finite domains. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. QANARY, our structural dependency analysis framework, verified 1.17 million cells across 30 modules of the Adams Bridge ML-DSA/ML-KEM accelerator [3, 4], but its core soundness result (Theorem 3.9.1) was machine-checked only at $q = 5$ via $2^{25}$ Boolean wire functions. This left portability to ML-KEM ($q = 3{,}329$, FIPS 203 [5]) and ML-DSA ($q = 8{,}380{,}417$, FIPS 204 [6]) as an open gap. NIST IR 8547 [7] (March 2025) motivates closing such gaps. We present the first machine-checked universal proof of the $r$-free sub-theorem of Theorem 3.9.1: for every $q > 0$, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. The proof, in Lean 4 [8] with Mathlib [9], requires five lines versus $2^{25}$ finite evaluations. It is sorry-free, reducing the trusted base from {Z3 [10], CVC5 [11], Python} to the Lean 4 kernel. We provide nine theorems (T1--T6, T1', T3') covering reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample for all $q \geq 2$. The results establish commutative ring axioms of $\mathbb{Z}/q\mathbb{Z}$ as the natural abstraction layer for arithmetic masking verification.
• Abstract（参考訳）: ポスト量子暗号(PQC)ハードウェアにおけるマスキングの形式的検証は、有限領域上のSMTソルバに依存する。 我々の以前の研究はスケール[1]で構造依存性解析を確立し、部分NTTマスキングのセキュリティマージンを定量化した[2]。 構造依存性分析フレームワークであるQANaryは、Adams Bridge ML-DSA/ML-KEMアクセラレーター[3, 4]の30個のモジュールにまたがる117万セルを検証したが、その中核となる音質結果(Theorem 3.9.1)は、わずか$q = 5$ via $2^{25}$ Booleanワイヤ関数でしかマシンチェックされなかった。 これにより ML-KEM (q = 3{,}329$, FIPS 203 [5]) と ML-DSA (q = 8{,}380{,}417$, FIPS 204 [6]) がオープンギャップとして残った。 NIST IR 8547 [7] (2025年3月) はそのようなギャップを埋める動機となっている。 我々は、Theorem 3.9.1: for every $q > 0$, every wire function and every pair of secrets, value-independence suggests same marginal distributions。 この証明は、Mathlib [9] のLean 4[8] では、5行に対して 2^{25}$ の有限評価が必要です。 信頼されたベースを {Z3 [10], CVC5 [11], Python} から Lean 4 カーネルに還元するのは残念なことだ。 我々は9つの定理(T1--T6, T1', T3')を提供し、すべての$q \geq 2$に対して再パラメータ化、単射性、オーバーフロー境界、RNGバイアス、および普遍的非重みのない反例をカバーしている。 その結果、算術マスキング検証の自然な抽象層として$\mathbb{Z}/q\mathbb{Z}$の可換環公理が成立する。

関連論文リスト

• Optimal Scalar Quantization for Matrix Multiplication: Closed-Form Density and Phase Transition [50.36362492608702]
  乗算前の2つの行列のエントリーワイズスカラー量子化について検討した。 我々は、閉形式の最適点密度 [ star(u) propto exp!left(-fracu26right)bigl( (1-2)+2u22bigr), qquad u=fracx_X を求め、相関駆動相転移を証明した。
  論文  参考訳（メタデータ） (2026-03-20T01:53:44Z)
• Rényi exponent landscape of multipartite entanglement in free-fermion systems [51.56484100374058]
  我々は、Rényi tripartite information $I_3() が小フェルミ運動量での質的に $exclusion-dependent scaling を示すことを示した。 I_m(n)/I_m(1) sim zm-1 to 0$ for all integer $n geq 2$, so the leading von Neumann signal can builded from integer Rényi data。
  論文  参考訳（メタデータ） (2026-03-09T22:27:00Z)
• The Spectral Dimension of NTKs is Constant: A Theory of Implicit Regularization, Finite-Width Stability, and Scalable Estimation [0.0]
  定数極限法則 $lim_ntoinfty mathbbE[r_texteff(K_n)] = mathbbE[k(x, x)]2 を証明する。 有限幅 NTK が作用素ノルムにおいて $O_p(m-1/2)$ でずれるなら、$r_texteff$ は $O_p(m-1/2)$ で変化する。 ランダムを用いたスケーラブルな推定器を設計する
  論文  参考訳（メタデータ） (2025-11-30T12:14:21Z)
• Algebraic Obstructions and the Collapse of Elementary Structure in the Kronecker Problem [0.0]
  マーナハンの基礎研究から87年間、真に3列のケースに対して明確な閉形式の公式は得られていない。 階段-フック係数の明示的な公式を5つ導き、サクセル予想を132個の三列分割で検証する。 連続閉塞と離散積分性の間の張力を利用した証明手法である整数強制法を開発した。
  論文  参考訳（メタデータ） (2025-11-28T03:21:01Z)
• Clifford quantum cellular automata from topological quantum field theories and invertible subalgebras [10.600087006666332]
  本稿では、トポロジカル量子場理論(TQFT)と非可逆部分代数(ISA)から量子セルオートマトン(QCA)を構築するための枠組みを提案する。 このアプローチは、すべての許容次元におけるすべての $mathbbZ$ と $mathbbZ_p$ クリフォード QCA を明示的に実現する。
  論文  参考訳（メタデータ） (2025-09-08T18:00:13Z)
• Quantum-Resistant RSA Modulus Decomposition via Adaptive Rényi Entropy Optimization [0.0]
  本稿では,RSAの量子攻撃に対する耐性を高めるための理論的アプローチについて検討する。 我々は素数が制御された近接で生成される枠組みを開発する。 主な貢献は、素分布特性と量子攻撃複雑性の接続を確立することである。
  論文  参考訳（メタデータ） (2025-07-04T11:18:34Z)
• A Unified Framework for Uniform Signal Recovery in Nonlinear Generative Compressed Sensing [68.80803866919123]
  非線形測定では、ほとんどの先行結果は一様ではない、すなわち、すべての$mathbfx*$に対してではなく、固定された$mathbfx*$に対して高い確率で保持される。 本フレームワークはGCSに1ビット/一様量子化観測と単一インデックスモデルを標準例として適用する。 また、指標集合が計量エントロピーが低い製品プロセスに対して、より厳密な境界を生み出す濃度不等式も開発する。
  論文  参考訳（メタデータ） (2023-09-25T17:54:19Z)
• Average-Case Complexity of Tensor Decomposition for Low-Degree Polynomials [93.59919600451487]
  多くの統計的推論タスクにおいて「統計計算ギャップ」が発生する。 1つの成分が他の成分よりもわずかに大きいランダムオーダー3分解モデルを考える。 テンソルエントリは$ll n3/2$のとき最大成分を正確に推定できるが、$rgg n3/2$のとき失敗する。
  論文  参考訳（メタデータ） (2022-11-10T00:40:37Z)
• Learning a Single Neuron with Adversarial Label Noise via Gradient Descent [50.659479930171585]
  モノトン活性化に対する $mathbfxmapstosigma(mathbfwcdotmathbfx)$ の関数について検討する。 学習者の目標は仮説ベクトル $mathbfw$ that $F(mathbbw)=C, epsilon$ を高い確率で出力することである。
  論文  参考訳（メタデータ） (2022-06-17T17:55:43Z)

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

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