論文の概要: Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

• arxiv url: http://arxiv.org/abs/2604.25878v1
• Date: Tue, 28 Apr 2026 17:21:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-29 16:49:17.972121
• Title: Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking
• Title（参考訳）: Prime-Field PINI:ポスト量子NTTマスキングのための機械式合成理論
• Authors: Ray Iskander, Khaled Kirah,
• Abstract要約: 我々は、我々の知る限り、素体上の算術マスキングのための最初の機械チェックされた合成定理を証明した。 パラメータが$k_$と$k$の2つのPF-PINIガジェットの場合、合成された2段パイプラインは、PF-PINI($k$)を満たす。 バレット還元の代数とハードウェアに忠実な算術モデルを正式にブリッジし、定理をインスタンス化し、MicrosoftのAdams Bridge PQCアクセラレーターを診断する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This is Paper 6 of a series of formally-verified analyses of masked NTT hardware for post-quantum cryptography; Paper 1 [1] established structural dependency analysis of the QANARY platform, and Paper 2 [2] quantified security margins under partial NTT masking. Boolean masking composition is well-understood through NI, SNI, and PINI. Arithmetic masking over $\mathbb{Z}_q$ for prime $q$, the foundation of NTT-based post-quantum cryptography, has lacked an analogous theory. We prove, to our knowledge, the first machine-checked composition theorems for arithmetic masking over prime fields. Our key insight is the renewal argument: when a fresh random mask is applied between two pipeline stages, the intermediate wire becomes perfectly uniform regardless of Stage 1's security parameter. For two PF-PINI gadgets with parameters $k_1$ and $k_2$, the composed two-stage pipeline with fresh masking satisfies PF-PINI($k_2$), Stage 1's multiplicity is completely erased from the composed output. Without fresh masking, intermediate wires have multiplicity up to $k_1$, creating a necessary condition for differential power analysis. We formalize both theorems in Lean 4 with 18 machine-checked proofs and zero sorry stubs. We formally bridge the algebraic and hardware-faithful arithmetic models of Barrett reduction, and instantiate the theorems to formally diagnose Microsoft's Adams Bridge PQC accelerator: its absence of fresh inter-stage masking leaves Barrett output wires non-uniform under the first-order probing model, the same architectural flaw that two independent empirical analyses [3, 4] and our own prior structural analysis [1] identified. Computational evidence further suggests the 1-Bit Barrier is universal across Barrett and Montgomery reductions.
• Abstract（参考訳）: 本論文は、量子後暗号のためのマスク付きNTTハードウェアの一連の公式検証分析の論文6、QANaryプラットフォームの構造依存性解析の論文1[1]、部分NTTマスキングによるセキュリティマージンの定量化に関する論文2[2]である。 ブールマスク組成物は、NI、SNI、PINIを介してよく理解されている。 NTTベースのポスト量子暗号の基礎である素数$q$の$\mathbb{Z}_q$に対する算術マスクは、類似した理論を欠いている。 我々は、我々の知る限り、素体上の算術マスキングのための最初の機械チェックされた合成定理を証明した。 新たなランダムマスクが2つのパイプラインステージの間に適用されると、中間ワイヤはステージ1のセキュリティパラメータに関係なく完全に均一になる。 パラメータが$k_1$と$k_2$の2つのPF-PINIガジェットの場合、合成された2段パイプラインは、PF-PINI($k_2$)を満たす。 新たなマスキングがなければ、中間線は最大$k_1$の多重性を持ち、差分電力解析に必要な条件を生成する。 両定理をLean 4で形式化し、18のマシンチェックによる証明と、残念なスタブをゼロにします。 我々はバレット還元の代数的およびハードウェアに忠実な算術モデルを正式にブリッジし、MicrosoftのアダムスブリッジPQC加速器を正式に診断するための定理をインスタンス化する。 さらに計算上の証拠は、バレットとモンゴメリーの減量で1ビットバリアが普遍的であることを示唆している。

関連論文リスト

• Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware [0.0]
  バレットリダクションはNTTベースのポスト量子暗号実装のすべての非線形コアである。 既存の構成フレームワークはGF(2)上のマスキングに対処している。 PF-PINIはPF-PINI(2)を満たす。
  論文  参考訳（メタデータ） (2026-04-27T16:27:33Z)
• 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)
• Cloning Games, Black Holes and Cryptography [50.022147589030304]
  クローンゲーム解析のための新しいツールキットを提案する。 このフレームワークにより、バイナリフェーズ状態に基づいて新しいクローンゲームを分析することができる。 連成位相の変分最適境界は、ブラックホールの理想化されたモデルで衝突する情報について定量的な洞察を与えることを示す。
  論文  参考訳（メタデータ） (2024-11-07T14:09:32Z)
• The Power of Unentangled Quantum Proofs with Non-negative Amplitudes [55.90795112399611]
  非負の振幅を持つ非絡み合った量子証明のパワー、つまり $textQMA+(2)$ を表すクラスについて研究する。 特に,小集合拡張,ユニークなゲーム,PCP検証のためのグローバルプロトコルを設計する。 QMA(2) が $textQMA+(2)$ に等しいことを示す。
  論文  参考訳（メタデータ） (2024-02-29T01:35:46Z)
• On sampling determinantal and Pfaffian point processes on a quantum computer [49.1574468325115]
  DPPは1970年代の量子光学のモデルとしてマッキによって導入された。 ほとんどのアプリケーションはDPPからのサンプリングを必要としており、その量子起源を考えると、古典的なコンピュータでDPPをサンプリングするのは古典的なものよりも簡単かどうか疑問に思うのが自然である。 バニラサンプリングは、各コスト$mathcalO(N3)$と$mathcalO(Nr2)$の2つのステップから構成される。
  論文  参考訳（メタデータ） (2023-05-25T08:43:11Z)
• The Sample Complexity of One-Hidden-Layer Neural Networks [57.6421258363243]
  本研究では,スカラー値を持つ一層ネットワークのクラスとユークリッドノルムで有界な入力について検討する。 隠蔽層重み行列のスペクトルノルムの制御は、一様収束を保証するには不十分であることを示す。 スペクトルノルム制御が十分であることを示す2つの重要な設定を解析する。
  論文  参考訳（メタデータ） (2022-02-13T07:12:02Z)

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

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