論文の概要: Formally-verified Security against Forgery of Remote Attestation using SSProve

• arxiv url: http://arxiv.org/abs/2502.17653v1
• Date: Mon, 24 Feb 2025 21:02:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-26 15:20:30.139317
• Title: Formally-verified Security against Forgery of Remote Attestation using SSProve
• Title（参考訳）: SSProveを用いた遠隔検診の偽造に対する形式的検証
• Authors: Sara Zain, Jannik Mähn, Stefan Köpsell, Sebastian Ertel,
• Abstract要約: 本稿では,RAの基本セキュリティ特性の機械的形式化について述べる。 まずデジタルシグネチャを定義し、強力な存在攻撃モデルにおいて、偽造に対するセキュリティを正式に検証する。 我々の開発は、RAプロトコルが偽造に対して安全であることを示す証拠を提供する。
• 参考スコア（独自算出の注目度）: 0.21427777919040417
• License:
• Abstract: Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of State-Separating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures. Finally, we found that proving the security of the primitives for digital signatures was not feasible. This observation contrasts textbook formalizations and sparks a discussion on reasoning about the security of libraries in SSP-based frameworks.
• Abstract（参考訳）: リモートテスト(RA)は、クラウド上での信頼性の高い実行環境と、オペレーティングシステムでオンボードされる信頼性の高いデバイスドライバの基礎である。 しかし、RAは、そのセキュリティ特性の厳密な機械的定義を最も強いモデルの一つ、すなわちセマンティックモデルで見逃している。 このような機械化は国家分離証明(SSP)の概念を必要とする。 しかし、SSPはRocq Proverの基盤フレームワークとして実装されたばかりであった。 本稿では,RAの基本セキュリティ特性の機械的形式化について述べる。 我々のRocq Prover開発は、まずデジタル署名を定義し、強力な存在的攻撃モデルにおける偽造に対するセキュリティを正式に検証します。 これらの結果に基づき、RAを定義し、RAのセキュリティをデジタル署名のセキュリティに還元する。 我々の開発は、RAプロトコルが偽造に対して安全であることを示す証拠を提供する。 さらに、私たちの推論をRAのプリミティブに拡張し、デジタルシグネチャのプリミティブのセキュリティに対するセキュリティを低減します。 最後に、デジタル署名のプリミティブのセキュリティを証明することは不可能であることがわかった。 この観察は、教科書の形式化とは対照的であり、SSPベースのフレームワークにおけるライブラリのセキュリティに関する推論に関する議論を引き起こしている。

関連論文リスト

• Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  認証サイクル冗長性チェック(ACRIC)を提案する。 ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。 ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
  論文  参考訳（メタデータ） (2024-11-21T18:26:05Z)
• VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
  CHERIはハードウェアに直接、きめ細かいメモリ保護を提供し、強制する。 VeriCHERIはISA仕様を一切必要としないという点で、従来のものと概念的に異なる。 CHERIの変種を実装したRISC-Vベースのプロセッサ上で,VeriCHERIの有効性とスケーラビリティを示す。
  論文  参考訳（メタデータ） (2024-07-26T11:48:55Z)
• On the Design and Security of Collective Remote Attestation Protocols [5.01030444913319]
  Collective Remote Attestation (CRA)は、(異種)ネットワークにおいて、侵入されたデバイスを効率的に識別することを目的としたセキュリティサービスである。 ここ数年、CRAプロトコルの提案が大幅に増加し、様々なネットワークトポロジによってガイドされた様々な設計が示されている。 CRAプロトコルを体系的に比較可能な統合フレームワークであるCatを提示する。
  論文  参考訳（メタデータ） (2024-07-12T12:06:49Z)
• Generalized Quantum-assisted Digital Signature [2.187441808562386]
  本稿では,デジタル署名のためにQKDキーを採用することで,情報理論のセキュリティを継承する手法の改良版を提案する。 偽造に対するセキュリティは、悪意のある偽造者によって取られた試行錯誤アプローチを考慮して計算され、GQaDSパラメータは偽造と鑑定確率のバランスをとる分析的アプローチによって最適化される。
  論文  参考訳（メタデータ） (2024-06-28T15:04:38Z)
• Towards Credential-based Device Registration in DApps for DePINs with ZKPs [46.08150780379237]
  ブロックチェーン上のデバイス認証を検証するクレデンシャルベースのデバイス登録(CDR)機構を提案する。 本稿では,Groth16 と Marlin を用いた zkSNARK を用いた汎用システムモデルを提案し,CDR を技術的に評価する。
  論文  参考訳（メタデータ） (2024-06-27T09:50:10Z)
• Poisoning Prevention in Federated Learning and Differential Privacy via Stateful Proofs of Execution [8.92716309877259]
  フェデレートラーニング(FL)とローカルディファレンシャルプライバシ(LDP)は、ここ数年で多くの注目を集めています。 彼らは毒殺攻撃に弱いという共通の制限を共有している。 本稿では,国家執行の証明という新たなセキュリティ概念に基づいて,この問題を是正するシステムレベルのアプローチを提案する。
  論文  参考訳（メタデータ） (2024-04-10T04:18:26Z)
• A Zero Trust Framework for Realization and Defense Against Generative AI Attacks in Power Grid [62.91192307098067]
  本稿では電力グリッドサプライチェーン(PGSC)のための新しいゼロ信頼フレームワークを提案する。 潜在的なGenAIによる攻撃ベクターの早期発見、テールリスクに基づく安定性の評価、そしてそのような脅威の緩和を容易にする。 実験の結果,ゼロ信頼フレームワークは攻撃ベクトル生成に95.7%の精度,95%安定PGSCに9.61%のリスク尺度,GenAIによる攻撃に対する防御に99%の信頼性が得られた。
  論文  参考訳（メタデータ） (2024-03-11T02:47:21Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。 TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。 本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
  論文  参考訳（メタデータ） (2023-11-24T18:54:00Z)
• Ring-A-Bell! How Reliable are Concept Removal Methods for Diffusion Models? [52.238883592674696]
  Ring-A-Bellは、T2I拡散モデルのためのモデルに依存しないレッドチームツールである。 これは、不適切なコンテンツの生成に対応する拡散モデルに対する問題的プロンプトを特定する。 この結果から,安全プロンプトベンチマークの操作により,既存の安全メカニズムを回避できると考えられるプロンプトを変換できることが示唆された。
  論文  参考訳（メタデータ） (2023-10-16T02:11:20Z)

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

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