論文の概要: User-Guided Verification of Security Protocols via Sound Animation

• arxiv url: http://arxiv.org/abs/2410.00676v1
• Date: Tue, 1 Oct 2024 13:34:35 GMT
• ステータス: 処理完了
• システム内更新日: 2024-11-05 04:25:20.164730
• Title: User-Guided Verification of Security Protocols via Sound Animation
• Title（参考訳）: 音響アニメーションによるセキュリティプロトコルのユーザガイドによる検証
• Authors: Kangfeng Ye, Roberto Metere, Poonam Yadav,
• Abstract要約: 本稿では,対話木(ITrees)に基づくCSPの変種を用いたDolev-Yao攻撃モデルを実装し,プロトコルをアニメーターにコンパイルする。 コンパイルの健全性を保証するため、定理証明器 Isabelle/HOL で我々のアプローチを機械化した。
• 参考スコア（独自算出の注目度）: 3.094188181179751
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Current formal verification of security protocols relies on specialized researchers and complex tools, inaccessible to protocol designers who informally evaluate their work with emulators. This paper addresses this gap by embedding symbolic analysis into the design process. Our approach implements the Dolev-Yao attack model using a variant of CSP based on Interaction Trees (ITrees) to compile protocols into animators -- executable programs that designers can use for debugging and inspection. To guarantee the soundness of our compilation, we mechanised our approach in the theorem prover Isabelle/HOL. As traditionally done with symbolic tools, we refer to the Diffie-Hellman key exchange and the Needham-Schroeder public-key protocol (and Lowe's patched variant). We demonstrate how our animator can easily reveal the mechanics of attacks and verify corrections. This work facilitates security integration at the design level and supports further security property analysis and software-engineered integrations.
• Abstract（参考訳）: 現在のセキュリティプロトコルの正式な検証は、特殊な研究者や複雑なツールに依存しており、非公式にエミュレータを使った作業を評価するプロトコル設計者にはアクセスできない。 本稿では,シンボル解析を設計プロセスに組み込むことにより,このギャップを解消する。 当社のアプローチでは,インタラクションツリー(ITrees)に基づいたCSPの変種を用いて,Doulev-Yao攻撃モデルを実装して,プロトコルをアニメーターにコンパイルする。 コンパイルの健全性を保証するため、定理証明器 Isabelle/HOL で我々のアプローチを機械化した。 伝統的に象徴的なツールで行われているように、Diffie-Hellmanキー交換とNeedham-Schroeder公開鍵プロトコル(およびローのパッチ付き変種)を参照する。 我々は,我々のアニメーターが容易に攻撃のメカニズムを明らかにし,修正を検証できることを実証する。 この作業は、設計レベルでのセキュリティ統合を促進し、さらなるセキュリティプロパティ分析とソフトウェアエンジニアリング統合をサポートする。

関連論文リスト

• Strands Rocq: Why is a Security Protocol Correct, Mechanically? [3.6840775431698893]
  StrandsRocq は Coq のストランド空間の機械化である。 新しい証明技法と、新しい最大貫入器の概念が組み込まれている。 これは2つの単純な認証プロトコルに対するセキュリティの合成証明を提供する。
  論文  参考訳（メタデータ） (2025-02-18T13:34:58Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Games for AI Control: Models of Safety Evaluations of AI Deployment Protocols [52.40622903199512]
  本稿では,多目的かつ部分的に観察可能なゲームとして,AI-Control Gamesを紹介した。 我々は、信頼できない言語モデルをプログラミングアシスタントとしてデプロイするためのプロトコルをモデル化、評価、合成するために、フォーマリズムを適用した。
  論文  参考訳（メタデータ） (2024-09-12T12:30:07Z)
• EmInspector: Combating Backdoor Attacks in Federated Self-Supervised Learning Through Embedding Inspection [53.25863925815954]
  フェデレートされた自己教師付き学習(FSSL)は、クライアントの膨大な量の未ラベルデータの利用を可能にする、有望なパラダイムとして登場した。 FSSLはアドバンテージを提供するが、バックドア攻撃に対する感受性は調査されていない。 ローカルモデルの埋め込み空間を検査し,悪意のあるクライアントを検知する埋め込み検査器(EmInspector)を提案する。
  論文  参考訳（メタデータ） (2024-05-21T06:14:49Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
  論文  参考訳（メタデータ） (2024-05-09T19:57:59Z)
• Attack Tree Generation via Process Mining [0.0]
  本研究の目的は,攻撃ログからアタックツリーを自動的に生成する方法を提供することである。 このアプローチの主な特徴は、アタックツリーを合成するためにプロセスマイニングアルゴリズムを使用することである。 我々のアプローチは、モデルの導出と翻訳とは別に、ユーザがRisQFLanフォーマットでアタックツリーを提供するプロトタイプによってサポートされています。
  論文  参考訳（メタデータ） (2024-02-19T10:55:49Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Performance-lossless Black-box Model Watermarking [69.22653003059031]
  本稿では,モデル知的財産権を保護するために,ブランチバックドアベースのモデル透かしプロトコルを提案する。 さらに,プロトコルに対する潜在的な脅威を分析し,言語モデルに対するセキュアで実現可能な透かしインスタンスを提供する。
  論文  参考訳（メタデータ） (2023-12-11T16:14:04Z)
• Design for Assurance: Employing Functional Verification Tools for Thwarting Hardware Trojan Threat in 3PIPs [13.216074408064117]
  サードパーティの知的財産コアは、現代のシステムオンチップと集積回路の設計において必須の構成要素である。 これらの設計コンポーネントは通常、異なる信頼レベルを持つベンダーから来ており、文書化されていない設計機能を含んでいる可能性がある。 ハードウェア設計者になじみのある機能検証ツールや言語を用いて,ハードウェアトロイの木馬の識別と防止を行う手法を開発した。
  論文  参考訳（メタデータ） (2023-11-21T03:32:07Z)
• Software Vulnerability Detection via Deep Learning over Disaggregated Code Graph Representation [57.92972327649165]
  この研究は、コードコーパスから安全でないパターンを自動的に学習するためのディープラーニングアプローチを探求する。 コードには解析を伴うグラフ構造が自然に認められるため,プログラムの意味的文脈と構造的規則性の両方を利用する新しいグラフニューラルネットワーク(GNN)を開発する。
  論文  参考訳（メタデータ） (2021-09-07T21:24:36Z)
• Autoencoding Variational Autoencoder [56.05008520271406]
  我々は,この行動が学習表現に与える影響と,自己整合性の概念を導入することでそれを修正する結果について検討する。 自己整合性アプローチで訓練されたエンコーダは、敵攻撃による入力の摂動に対して頑健な(無神経な)表現につながることを示す。
  論文  参考訳（メタデータ） (2020-12-07T14:16:14Z)

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

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