論文の概要: Formal Verification of Probing Security via Conditional Independence

• arxiv url: http://arxiv.org/abs/2605.23316v1
• Date: Fri, 22 May 2026 07:34:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-25 17:29:20.240987
• Title: Formal Verification of Probing Security via Conditional Independence
• Title（参考訳）: 条件付き独立による保証の形式的検証
• Authors: Satoshi Kura, Katsuyuki Takashima,
• Abstract要約: サイドチャネル攻撃は暗号システムのセキュリティにとって大きな脅威である。 マスキングはこのような攻撃に対して広く用いられている対策であるが、マスクされたアルゴリズムの安全性を証明することは、正式な検証なしにエラーを起こしやすい。 本稿では,確率的分離論理に基づくマスク付きアルゴリズムの非干渉特性の形式的検証手法を提案する。
• 参考スコア（独自算出の注目度）: 0.14323566945483493
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Side-channel attacks are a major threat to the security of cryptosystems. Masking is a widely used countermeasure against such attacks, but proving the security of masked algorithms is error-prone without formal verification. In this work, we propose a novel approach to formal verification of noninterference properties of masked algorithms based on probabilistic separation logic. By establishing a connection between noninterference and conditional independence, we show how noninterference can be verified using Lilac, a separation logic for conditional independence. We also provide several proof rules that facilitate the verification of probing security and demonstrate their application to example algorithms.
• Abstract（参考訳）: サイドチャネル攻撃は暗号システムのセキュリティにとって大きな脅威である。 マスキングはこのような攻撃に対して広く用いられている対策であるが、マスクされたアルゴリズムの安全性を証明することは、正式な検証なしにエラーを起こしやすい。 本研究では,確率的分離論理に基づくマスク付きアルゴリズムの非干渉特性の形式的検証手法を提案する。 非干渉と条件独立の接続を確立することにより、条件独立のための分離論理であるLilacを用いて、非干渉がいかに検証できるかを示す。 また,セキュリティの検証を容易にするための証明ルールもいくつか提供し,その適用例を示す。

関連論文リスト

• Rigorous Security Proofs for Practical Quantum Key Distribution [0.0]
  この論文は量子鍵分配(QKD)プロトコルの厳密なセキュリティ解析に関係している。 IID集団攻撃に対する可変長QKDプロトコルのセキュリティ証明を確立し、この結果をポストセレクション手法を用いてコヒーレント攻撃に拡張する。 第2に,このプロトコルの観測統計値のみを用いて,エントロピー不確実性関係に基づく位相誤差率と位相誤差率に基づく証明の有界化手法を開発した。 第3に、限界制約付きエントロピー累積定理に基づく、非常に一般的なセキュリティ解析を示す。
  論文  参考訳（メタデータ） (2026-04-23T15:48:02Z)
• Protecting Context and Prompts: Deterministic Security for Non-Deterministic AI [0.0]
  大規模言語モデル(LLM)アプリケーションは、インジェクションやコンテキスト操作の攻撃に対して脆弱である。 我々は,暗号的に検証可能な証明を提供する2つの新しいプリミティブ(認証プロンプト)と認証コンテキスト(認証コンテキスト)を導入する。 プロトコルレベルのビザンチン抵抗を与える4つの証明された定理を持つポリシー代数を定式化する。
  論文  参考訳（メタデータ） (2026-02-11T03:38:59Z)
• VeriLLM: A Lightweight Framework for Publicly Verifiable Decentralized Inference [3.8760740008451156]
  本稿では,分散言語モデル (LLM) 推論のための公開検証プロトコルであるVeriLLMを紹介する。 VeriLLMは、軽量な経験的再実行と暗号的なコミットメントを組み合わせることで、検証者は基礎となる推論コストの約1%で結果を検証することができる。 We show that VeriLLM achieve reliable public verifiability with least overhead。
  論文  参考訳（メタデータ） (2025-09-29T04:07:32Z)
• Quantum Bayesian inference with Suport vector states for intrusion detection [0.0]
  本稿では,侵入検出のための量子ベイズ推定法を提案する。 この方法は、因果構造に整合した関節、縁、条件付き確率を与える。 本研究は,情報セキュリティアプリケーションにおける量子ネイティブ推論の実現可能性と解釈性を示すものである。
  論文  参考訳（メタデータ） (2025-07-01T03:41:04Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• Token-Level Adversarial Prompt Detection Based on Perplexity Measures and Contextual Information [67.78183175605761]
  大規模言語モデルは、敵の迅速な攻撃に影響を受けやすい。 この脆弱性は、LLMの堅牢性と信頼性に関する重要な懸念を浮き彫りにしている。 トークンレベルで敵のプロンプトを検出するための新しい手法を提案する。
  論文  参考訳（メタデータ） (2023-11-20T03:17:21Z)
• Spatial-Frequency Discriminability for Revealing Adversarial Perturbations [53.279716307171604]
  敵の摂動に対するディープニューラルネットワークの脆弱性は、コンピュータビジョンコミュニティで広く認識されている。 現在のアルゴリズムは、通常、自然および敵対的なデータの識別的分解を通じて、敵のパターンを検出する。 空間周波数Krawtchouk分解に基づく識別検出器を提案する。
  論文  参考訳（メタデータ） (2023-05-18T10:18:59Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• Logically Sound Arguments for the Effectiveness of ML Safety Measures [0.1657441317977376]
  本稿では,機械学習機能の安全性に関する議論において,十分な厳格性を達成するための課題について検討する。 安全目標に関連付けることにより,不正確な歩行者位置決めの指標を明確化する。 次に,ポストプロセッサの有効性を議論するための半形式保証事例を提案する。
  論文  参考訳（メタデータ） (2021-11-04T06:09:34Z)

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

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