論文の概要: Automated Side-Channel Analysis of Cryptographic Protocol Implementations

• arxiv url: http://arxiv.org/abs/2511.11385v2
• Date: Mon, 17 Nov 2025 15:36:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-18 14:36:22.677779
• Title: Automated Side-Channel Analysis of Cryptographic Protocol Implementations
• Title（参考訳）: 暗号プロトコル実装のサイドチャネル自動解析
• Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati,
• Abstract要約: WhatsAppの最初の形式モデルを実装から抽出する。 コンパイル後セキュリティに対する既知のクローンアタックを特定します。 本稿では,暗号プロトコルの実装をサイドチャネル攻撃に対するレジリエンスとして解析する手法を提案する。
• 参考スコア（独自算出の注目度）: 9.38081874899831
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We extract the first formal model of WhatsApp from its implementation by combining binary-level analysis (via CryptoBap) with reverse engineering (via Ghidra) to handle this large closed-source application. Using this model, we prove forward secrecy, identify a known clone-attack against post-compromise security and discover functional gaps between WhatsApp's implementation and its specification. We further introduce a methodology to analyze cryptographic protocol implementations for their resilience to side-channel attacks. This is achieved by extending the CryptoBap framework to integrate hardware leakage contracts into the protocol model, which we then pass to the state-of-the-art protocol prover, DeepSec. This enables a detailed security analysis against both functional bugs and microarchitectural side-channel attacks. Using this methodology, we identify a privacy attack in WhatsApp that allows a side-channel attacker to learn the victim's contacts and confirm a known unlinkability attack on the BAC protocol used in electronic passports. Key contributions include (1) the first formal model of WhatsApp, extracted from its binary, (2) a framework to integrate side-channel leakage contracts into protocol models for the first time, and (3) revealing critical vulnerabilities invisible to specification-based methods.
• Abstract（参考訳）: この大規模なクローズドソースアプリケーションを扱うために、バイナリレベルの分析(CryptoBap経由)とリバースエンジニアリング(Ghidra経由)を組み合わせることで、WhatsAppの最初の形式モデルを実装から抽出する。 このモデルを用いて、フォワードシークレットを証明し、コンパイル後セキュリティに対する既知のクローンアタックを特定し、WhatsAppの実装と仕様の間の機能的ギャップを発見する。 さらに、サイドチャネル攻撃に対するレジリエンスのための暗号プロトコルの実装を分析する手法についても紹介する。 これはCryptoBapフレームワークを拡張して、ハードウェアリーク契約をプロトコルモデルに統合することで実現されます。 これにより、機能バグとマイクロアーキテクチャサイドチャネル攻撃の両方に対する詳細なセキュリティ分析が可能になる。 この手法を用いることで、WhatsAppのプライバシ攻撃を特定し、サイドチャネル攻撃者が被害者の連絡先を学習し、電子パスポートで使用されるBACプロトコルに対する既知の非リンク性攻撃を確認する。 主なコントリビューションとしては、(1)バイナリから抽出されたWhatsAppの最初の形式モデル、(2)サイドチャネルリーク契約をプロトコルモデルに初めて統合するフレームワーク、(3)仕様ベースのメソッドで見えない重要な脆弱性を明らかにすることなどがある。

関連論文リスト

• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。 以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。 我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
  論文  参考訳（メタデータ） (2025-08-26T20:59:16Z)
• The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version) [6.595258607341775]
  我々はプロトコルの実装をプロトコルの実装と残りの実装に分割する*Diodon*と呼ばれる方法論を開発します。 この分割により、セキュリティクリティカルなCoreに強力な半自動検証技術を適用することができます。 完全な自動静的解析は、アプリケーションがCoreで証明されたセキュリティプロパティを無効にできないことを保証することで、検証全体を拡張します。 署名付きDiffie-Hellmanキー交換の実装と、キー交換プロトコルを実装する大規模(100k+LoC)プロダクションGoの2つのケーススタディでDiodonを評価した。
  論文  参考訳（メタデータ） (2025-07-01T09:25:54Z)
• CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
  パーソナライズされた暗号化手法に基づく新しいジェイルブレイクフレームワークであるCodeChameleonを提案する。 我々は、7つの大規模言語モデルに関する広範な実験を行い、最先端の平均アタック成功率(ASR)を達成する。 GPT-4-1106上で86.6%のASRを実現する。
  論文  参考訳（メタデータ） (2024-02-26T16:35:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Protecting Model Adaptation from Trojans in the Unlabeled Data [120.42853706967188]
  本稿では,よく設計された毒物標的データによるモデル適応に対するトロイの木馬攻撃の可能性について検討する。 本稿では,既存の適応アルゴリズムとシームレスに統合可能なDiffAdaptというプラグイン・アンド・プレイ手法を提案する。
  論文  参考訳（メタデータ） (2024-01-11T16:42:10Z)
• Performance-lossless Black-box Model Watermarking [69.22653003059031]
  本稿では,モデル知的財産権を保護するために,ブランチバックドアベースのモデル透かしプロトコルを提案する。 さらに,プロトコルに対する潜在的な脅威を分析し,言語モデルに対するセキュアで実現可能な透かしインスタンスを提供する。
  論文  参考訳（メタデータ） (2023-12-11T16:14:04Z)
• CryptoBap: A Binary Analysis Platform for Cryptographic Protocols [6.514727189942011]
  暗号プロトコルの弱い秘密と認証を検証するプラットフォームであるCryptoBapを紹介する。 まずプロトコルのバイナリを中間表現に変換し、次に暗号対応のシンボル実行を実行する。 提案手法の健全性を実証し,CryptoBapを用いて,おもちゃの例から実世界のプロトコルまで,複数のケーススタディを検証した。
  論文  参考訳（メタデータ） (2023-08-28T09:41:45Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• Dispelling Myths on Superposition Attacks: Formal Security Model and Attack Analyses [0.0]
  マルチパーティプロトコルの重ね合わせ攻撃を考慮した最初の計算セキュリティモデルを提案する。 我々の新しいセキュリティモデルは、よく知られたOne-Time-Padプロトコルのセキュリティを証明することで満足できることを示す。 重畳攻撃に抵抗するセキュアな2要素計算のための最初の具体的なプロトコルを構築するために,この新たな知識を用いている。
  論文  参考訳（メタデータ） (2020-07-01T18:00:54Z)
• Mind the GAP: Security & Privacy Risks of Contact Tracing Apps [75.7995398006171]
  GoogleとAppleは共同で,Bluetooth Low Energyを使用した分散型コントラクトトレースアプリを実装するための公開通知APIを提供している。 実世界のシナリオでは、GAP設計は(i)プロファイリングに脆弱で、(ii)偽の連絡先を生成できるリレーベースのワームホール攻撃に弱いことを実証する。
  論文  参考訳（メタデータ） (2020-06-10T16:05:05Z)

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

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