論文の概要: The Matrix Reloaded: A Mechanized Formal Analysis of the Matrix Cryptographic Suite

• arxiv url: http://arxiv.org/abs/2408.12743v2
• Date: Sat, 07 Dec 2024 20:10:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-10 14:47:03.326572
• Title: The Matrix Reloaded: A Mechanized Formal Analysis of the Matrix Cryptographic Suite
• Title（参考訳）: マトリックスリロード:マトリックス暗号スイートの機械的形式解析
• Authors: Jacob Ginesin, Cristina Nita-Rotaru,
• Abstract要約: マトリックスで使用される暗号プロトコルであるOlmとMegolmについて検討する。 私たちはVerifpalを使ってオルムとメゴルムの形式モデルとそれらの構成を構築します。 我々はOlmとMegolmに関する様々な特性を証明し、認証、機密性、フォワード・シークレット、およびポスト・コンプロミズ・セキュリティを含む。
• 参考スコア（独自算出の注目度）: 9.013104500445491
• License:
• Abstract: Secure instant group messaging applications such as WhatsApp, Facebook Messenger, Matrix, and the Signal Application have become ubiquitous in today's internet, cumulatively serving billions of users. Unlike WhatsApp, for example, Matrix can be deployed in a federated manner, allowing users to choose which server manages their chats. To account for this difference in architecture, Matrix employs two novel cryptographic protocols: Olm, which secures pairwise communications, and Megolm, which relies on Olm and secures group communications. Olm and Megolm are similar to and share security goals with Signal and Sender Keys, which are widely deployed in practice to secure group communications. While Olm, Megolm, and Sender Keys have been manually analyzed in the computational model, no symbolic analysis nor mechanized proofs of correctness exist. Using mechanized proofs and computer-aided analysis is important for cryptographic protocols, as hand-written proofs and analysis are error-prone and often carry subtle mistakes. Using Verifpal, we construct formal models of Olm and Megolm, as well as their composition. We prove various properties of interest about Olm and Megolm, including authentication, confidentiality, forward secrecy, and post-compromise security. We also mechanize known limitations, previously discovered attacks, and trivial attacker wins from the specifications and previous literature. Finally, we model Sender Keys and the composition of Signal with Sender Keys in order to draw a comparison with Olm, Megolm, and their composition. From our analysis we conclude the composition of Olm and Megolm has comparable security to the composition of Signal and Sender Keys if Olm pre-keys are signed, and provably worse post-compromise security if Olm pre-keys are not signed.
• Abstract（参考訳）: WhatsApp、Facebook Messenger、Matrix、Signal Applicationといったセキュアなインスタントグループメッセージングアプリケーションは、今日のインターネットに広く浸透し、数十億のユーザに累積的なサービスを提供している。 例えばWhatsAppとは異なり、Matrixは連携した方法でデプロイでき、ユーザーはどのサーバーがチャットを管理するかを選択できる。 このアーキテクチャの違いを説明するため、MatrixはOlmと、Olmに依存してグループ通信をセキュアにするMegolmという2つの新しい暗号プロトコルを採用している。 OlmとMegolmはSignalとSender Keysと同様のセキュリティ目標を共有している。 Olm、Megolm、Sender Keysは計算モデルで手動で分析されているが、記号解析や機械化による正しさの証明は存在しない。 機械的証明とコンピュータ支援分析は、手書きの証明と分析がエラーを起こし、しばしば微妙な誤りを犯すため、暗号プロトコルにとって重要である。 Verifpal を用いて、Olm と Megolm の形式モデルとそれらの構成を構築します。 我々はOlmとMegolmに関する様々な特性を証明し、認証、機密性、フォワード・シークレット、およびポスト・コンプロミズ・セキュリティを含む。 また、既知の制限を機械化し、以前発見された攻撃と、明快な攻撃者が仕様と以前の文献から勝利する。 最後に、Sender KeysとSignal with Sender Keysの合成をモデル化し、Olm、Megolm、およびそれらの構成と比較する。 我々の分析から、Olm と Megolm の合成は、Olm プリキーが署名された場合、Signal と Sender Keys の合成と同等のセキュリティを持ち、Olm プリキーが署名されていなければ、明らかに、コンパイル後のセキュリティが悪化する。

関連論文リスト

• Secure Semantic Communication With Homomorphic Encryption [52.5344514499035]
  本稿では,SemCom に準同型暗号を適用する可能性について検討する。 タスク指向のSemComスキームを提案する。
  論文  参考訳（メタデータ） (2025-01-17T13:26:14Z)
• Secure Composition of Quantum Key Distribution and Symmetric Key Encryption [3.6678562499684517]
  量子鍵分布(QKD)により、アリスとボブは秘密鍵を秘密のチャネル上で共有し、物理法則にのみ拘束される敵に対する情報理論上のセキュリティを証明した。 セキュアな対称鍵ベース暗号アルゴリズムを用いたQKD確立鍵を用いた場合の問題点を考察し,ハイブリッド暗号に基づくアプローチを用いて構成の安全性の証明を行う。
  論文  参考訳（メタデータ） (2025-01-14T20:58:02Z)
• Echomix: a Strong Anonymity System with Messaging [0.0]
  Echomixは実践的なミックスネットワークフレームワークであり、関連するプロトコルのスイートである。 グローバルな敵による交通分析に対する抵抗によって、他の匿名システムと区別される。 レイテンシと帯域幅のオーバーヘッドが比較的低い。
  論文  参考訳（メタデータ） (2025-01-06T11:18:03Z)
• Quantum digital signature based on single-qubit without a trusted third-party [45.41082277680607]
  我々は、よりセキュリティを向上させるために、量子ビット技術のみを頼りにすることなく、新しい量子デジタル署名プロトコルを提案する。 また,このプロトコルは,非対称性,不確定性,拡張性など,他の重要な安全特性を満足する。
  論文  参考訳（メタデータ） (2024-10-17T09:49:29Z)
• 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)
• Defending Large Language Models against Jailbreak Attacks via Semantic Smoothing [107.97160023681184]
  適応型大規模言語モデル(LLM)は、ジェイルブレイク攻撃に対して脆弱である。 提案するSEMANTICSMOOTHは,与えられた入力プロンプトのセマンティック変換されたコピーの予測を集約するスムージングベースのディフェンスである。
  論文  参考訳（メタデータ） (2024-02-25T20:36:03Z)
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
  我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。 このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。 我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
  論文  参考訳（メタデータ） (2024-01-06T02:57:44Z)
• CCA-Secure Hybrid Encryption in Correlated Randomness Model and KEM Combiners [3.837357895668154]
  HE(Hybrid encryption)システムは、任意の長さのメッセージに対する効率的な公開鍵暗号システムである。 HE暗号化アルゴリズムは、KEM生成キーkを使用して、DEMを使用してメッセージをカプセル化する。 KEM/DEM合成定理 (KEM/DEM composition theorem) は、もし KEM と DEM が適切に定義されたセキュリティ概念を満たすなら、HE は適切に定義されたセキュリティで安全であることを証明している。
  論文  参考訳（メタデータ） (2024-01-02T01:16:52Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。 TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。 本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
  論文  参考訳（メタデータ） (2023-11-24T18:54:00Z)
• Randomized Message-Interception Smoothing: Gray-box Certificates for Graph Neural Networks [95.89825298412016]
  グラフニューラルネットワーク(GNN)のための新しいグレーボックス証明書を提案する。 我々はランダムにメッセージを傍受し、敵に制御されたノードからのメッセージがターゲットノードに到達する確率を分析する。 我々の証明書は、より遠くからの攻撃に対してより強力な保証を提供する。
  論文  参考訳（メタデータ） (2023-01-05T12:21:48Z)
• Dispelling Myths on Superposition Attacks: Formal Security Model and Attack Analyses [0.0]
  マルチパーティプロトコルの重ね合わせ攻撃を考慮した最初の計算セキュリティモデルを提案する。 我々の新しいセキュリティモデルは、よく知られたOne-Time-Padプロトコルのセキュリティを証明することで満足できることを示す。 重畳攻撃に抵抗するセキュアな2要素計算のための最初の具体的なプロトコルを構築するために,この新たな知識を用いている。
  論文  参考訳（メタデータ） (2020-07-01T18:00:54Z)

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

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