論文の概要: 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ハードウェアマスキング検証のためのリング理論の基礎
• 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}$の可換環公理が成立する。

関連論文リスト

• The I3322 quantum value is attained spatially but not in finite dimension [0.0]
  S$ をコリンズ・ギシン正規化の $I_3322$ Bell 関数の量子超越(古典的境界 0; 2量子ビット最大値 1/4)とする。 i) 有限次元の量子戦略が$S$(任意の有限局所次元、純粋または混合状態、射影またはPOVM測定)に達することはないこと、PalとVertesi(2010)を証明すること。 次元複雑性も決定する:$S_d$で局所次元$le d$と$D()=mind:S-S_dの最適値
  論文  参考訳（メタデータ） (2026-09-03T15:48:01Z)
• A phase transition in the exactness of the NPA hierarchy at the critical doubly-tilted CHSH functional [0.0]
  B_=langle A_0rangle+l B_0rangle+mathrmCHSH$。 すべての$,ge 1$とすべてのレベルで、階層は、アフィンのアイデンティティを実現する3つの明確な有理証明を通して、正確である。 サブクリティカル側では、正確な算術の最初の4つのレベルを認証する。
  論文  参考訳（メタデータ） (2026-07-15T12:34:25Z)
• Imbuing Large Language Models with Bidirectional Logic for Robust Chain Repair [44.80087038178069]
  本稿では,デコーダのみのトランスフォーマーをネイティブに組み込んだトレーニングフレームワークであるTeleological Reasoning Infilling (TRI)を紹介する。 推測では、TRIは二重システムループ内の外科的修復モジュールとして動作する。 3つのベンチマークの実験では、TRIは全てのタスクで最先端のパフォーマンスを達成し、プロブレム当たりのトークン支出を31.2%削減した。
  論文  参考訳（メタデータ） (2026-06-03T15:58:48Z)
• Module Lattice Security (Part IV): Probabilistic Polynomial Quantum Attack on Module-LWE over 2-Power Cyclotomics [1.0152838128195467]
  ML-KEMと関連する2パワーサイクロトミック格子スキームに対する量子攻撃を提案する。 ML-KEM-1024の近似係数は, ML-KEM-1024に対して$le 21 q/2=1664.5$を満たす。 解析を量子アルゴリズムを用いて2パワーのサイクロトミック環上でファルコン、ホーク、NTRUに拡張する。
  論文  参考訳（メタデータ） (2026-05-17T12:16:04Z)
• The Collapse of Unentangled Stoquastic Merlin-Arthur Proof Systems [46.657699628769336]
  絡み合いと干渉は量子力学の最も基本的な性質の一つである。 我々は絡み合いが確率的検証に余分な力を与えないことを証明する。
  論文  参考訳（メタデータ） (2026-05-15T17:52:33Z)
• What Do EEG Foundation Models Capture from Human Brain Signals? [64.48249643001402]
  現代の脳波基礎モデルは、自己教師付き事前訓練を通じて生信号から直接学習する。 我々は3つのサブクエストに分解する: モデルが何を学習するか、モデルを何に使用するのか、そしてどのように説明できるのか。 3つの基礎モデル(CSBrain, CBraMod, LaBraM),5つの臨床タスク(MDD, Stress, ISRUC-Sleep, TUSL, Siena)と6ファミリー63機能レキシコンを含む。
  論文  参考訳（メタデータ） (2026-05-12T01:57:53Z)
• Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking [0.0]
  我々は、我々の知る限り、素体上の算術マスキングのための最初の機械チェックされた合成定理を証明した。 パラメータが$k_$と$k$の2つのPF-PINIガジェットの場合、合成された2段パイプラインは、PF-PINI($k$)を満たす。 バレット還元の代数とハードウェアに忠実な算術モデルを正式にブリッジし、定理をインスタンス化し、MicrosoftのAdams Bridge PQCアクセラレーターを診断する。
  論文  参考訳（メタデータ） (2026-04-28T17:21:20Z)
• 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)
• 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)
• Two-way kernel matrix puncturing: towards resource-efficient PCA and spectral clustering [43.50783459690612]
  この方法は、データマトリックス$XinmathbbCptimes n$と対応するカーネル(Gram)マトリックス$K$の両方をBernoulliマスクを介してランダムに「切断」する。 我々は、GAN生成した画像データベースを実証的に確認し、データを劇的にパンクし、巨大な計算とストレージのゲインを提供することができることを確認した。
  論文  参考訳（メタデータ） (2021-02-24T14:01:58Z)

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

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