論文の概要: CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
- arxiv url: http://arxiv.org/abs/2305.12173v2
- Date: Fri, 5 Apr 2024 14:45:53 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-08 20:59:44.868582
- Title: CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
- Title(参考訳): CryptoVampire: 完全なシンボリック攻撃暗号モデルのための自動推論
- Authors: Simon Jeanteur, Laura Kovács, Matteo Maffei, Michael Rawson,
- Abstract要約: 我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。
主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。
理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
- 参考スコア(独自算出の注目度): 8.838422697156195
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols. A promising approach is given by the computationally complete symbolic attacker (CCSA), formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic analysis. The BC Logic is supported by a recently developed interactive theorem prover, Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge. We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. We overcome the burden of interactive proving in higher-order (HO) logic and automatically establish soundness of cryptographic protocols using only FO reasoning. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness. On the practical side, CryptoVampire integrates dedicated proof techniques using FO saturation algorithms and heuristics, which enable leveraging the state-of-the-art Vampire FO theorem prover as the underlying proving engine. Our experimental results show CryptoVampire's effectiveness of as a standalone verifier and in terms of automation support for Squirrel.
- Abstract(参考訳): 暗号プロトコルは、プロトコル標準でさえ、ますます増加する攻撃のリストで見られるように、設計と証明が困難である。
シンボリック・モデル(英語版)は、暗号化スキームの代数的性質を抽象化し、攻撃を見逃すような理想化されたモデルに対して、そのようなプロトコルの自動的なセキュリティ証明を可能にする。
計算モデルは厳密な保証を与えるが、現時点では対話的な証明と/または制限されたプロトコルのクラスのみをサポートする。
有望なアプローチは、BC論理で定式化された計算完全記号攻撃(CCSA)によって与えられる。
BC Logicは、最近開発されたインタラクティブな定理証明器であるSquirrelによってサポートされている。
我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。
主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。
我々は高階論理(HO)における対話的証明の負担を克服し、FO推論のみを用いて暗号プロトコルの健全性を自動的に確立する。
理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
実用面では、CryptoVampireはFO飽和アルゴリズムとヒューリスティックスを用いた専用の証明技術を統合しており、基礎となる証明エンジンとして最先端のヴァンパイアFO定理証明を活用できる。
実験結果から,CryptoVampireがスタンドアロンの検証器として有効であること,およびSquirrelの自動化サポートの観点から確認した。
関連論文リスト
- CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳(メタデータ) (2024-11-20T14:16:55Z) - The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。
しきい値暗号システムに対する既存のアプローチは、しきい値暗号プロトコルを実行するための少なくとも1つのメッセージ遅延の遅延オーバーヘッドを導入している。
しきい値が狭いブロックチェーンネイティブのしきい値暗号システムに対して,このオーバーヘッドを取り除く機構を提案する。
論文 参考訳(メタデータ) (2024-07-16T20:53:04Z) - Defending Large Language Models against Jailbreak Attacks via Semantic
Smoothing [107.97160023681184]
適応型大規模言語モデル(LLM)は、ジェイルブレイク攻撃に対して脆弱である。
提案するSEMANTICSMOOTHは,与えられた入力プロンプトのセマンティック変換されたコピーの予測を集約するスムージングベースのディフェンスである。
論文 参考訳(メタデータ) (2024-02-25T20:36:03Z) - CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
この文書はセキュリティプロトコル検証器CryptoVerifを示す。
これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。
自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
論文 参考訳(メタデータ) (2023-10-23T07:53:38Z) - CryptoBap: A Binary Analysis Platform for Cryptographic Protocols [6.514727189942011]
暗号プロトコルの弱い秘密と認証を検証するプラットフォームであるCryptoBapを紹介する。
まずプロトコルのバイナリを中間表現に変換し、次に暗号対応のシンボル実行を実行する。
提案手法の健全性を実証し,CryptoBapを用いて,おもちゃの例から実世界のプロトコルまで,複数のケーススタディを検証した。
論文 参考訳(メタデータ) (2023-08-28T09:41:45Z) - Perfectly Secure Steganography Using Minimum Entropy Coupling [60.154855689780796]
カチン1998のステガノグラフィー情報理論モデルでは, ステガノグラフィーの術式は完全に安全であることが示されている。
また, 完全セキュアな手順の中で, 最小エントロピー結合によって誘導される場合に限, 情報スループットが最大になることを示す。
論文 参考訳(メタデータ) (2022-10-24T17:40:07Z) - Cryptography with Certified Deletion [16.354530084834863]
我々は,暗号プリミティブの配列を認証された削除で生成する,新たな統一フレームワークを提案する。
プリミティブは、暗号化された平文が情報理論的に削除されたという古典的な証明書を生成するために、量子暗号文を保有している当事者を許可する。
論文 参考訳(メタデータ) (2022-07-05T00:48:06Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳(メタデータ) (2022-03-03T10:07:32Z) - Post-Quantum VRF and its Applications in Future-Proof Blockchain System [13.386254282693335]
検証可能なランダム関数 (VRF) は、その出力の正当性に対する非対話的に公に検証可能な証明を提供する強力な擬似ランダム関数である。
対称鍵プリミティブを用いた単純なVRFソリューションから量子後VRFを得るための汎用コンパイラを提案する。
量子セキュアなVRF(quantum-secure decentralized random beacon)の潜在的な応用例を示す。
論文 参考訳(メタデータ) (2021-09-05T07:10:41Z) - Spotting adversarial samples for speaker verification by neural vocoders [102.1486475058963]
我々は、自動話者検証(ASV)のための敵対サンプルを見つけるために、ニューラルボコーダを採用する。
元の音声と再合成音声のASVスコアの違いは、真正と逆正のサンプルの識別に良い指標であることがわかった。
私たちのコードは、将来的な比較作業のためにオープンソースにされます。
論文 参考訳(メタデータ) (2021-07-01T08:58:16Z) - Fast End-to-End Speech Recognition via a Non-Autoregressive Model and
Cross-Modal Knowledge Transferring from BERT [72.93855288283059]
LASO (Listen Attentively, and Spell Once) と呼ばれる非自動回帰音声認識モデルを提案する。
モデルは、エンコーダ、デコーダ、および位置依存集合体(PDS)からなる。
論文 参考訳(メタデータ) (2021-02-15T15:18:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。