論文の概要: CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)

• arxiv url: http://arxiv.org/abs/2310.14658v1
• Date: Mon, 23 Oct 2023 07:53:38 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-25 14:05:29.107784
• Title: CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)
• Title（参考訳）: CryptoVerif: 計算処理によるセキュリティプロトコル検証 (チャネル上で通信を行う初期バージョン)
• Authors: Bruno Blanchet,
• Abstract要約: この文書はセキュリティプロトコル検証器CryptoVerifを示す。 これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。 自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
• 参考スコア（独自算出の注目度）: 2.06682776181122
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This document presents the security protocol verifier CryptoVerif.CryptoVerif does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can verify secrecy, correspondence (which include authentication), and indistinguishability properties. It produces proofs presented as sequences of games, like those manually written by cryptographers; these games are formalized in aprobabilistic process calculus. CryptoVerif provides a generic method for specifying security properties of the cryptographic primitives.It produces proofs valid for any number of sessions of the protocol, and provides an upper bound on the probability of success of an attack against the protocol as a function of the probability of breaking each primitive and of the number of sessions. It can work automatically, or the user can guide it with manual proof indications.
• Abstract（参考訳）: この文書は、CryptoVerif.CryptoVerifはシンボリックなDolev-Yaoモデルではなく、計算モデルに依存しない。 機密性、対応性(認証を含む)、識別不能性を検証できる。 これは、暗号学者が手作業で書いたようなゲームのシーケンスとして提示される証明を生成し、これらのゲームは確率論的プロセス計算で形式化されている。 CryptoVerifは、暗号化プリミティブのセキュリティ特性を特定する汎用的な方法を提供し、プロトコルの任意のセッション数に有効な証明を生成し、プリミティブを破る確率とセッション数の確率の関数としてプロトコルに対する攻撃の確率の上限を提供する。 自動で動作させることもできるし、手動による証明表示でガイドすることもできる。

関連論文リスト

• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。 しきい値暗号システムに対する既存のアプローチは、しきい値暗号プロトコルを実行するための少なくとも1つのメッセージ遅延の遅延オーバーヘッドを導入している。 しきい値が狭いブロックチェーンネイティブのしきい値暗号システムに対して,このオーバーヘッドを取り除く機構を提案する。
  論文  参考訳（メタデータ） (2024-07-16T20:53:04Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• Provably Secure Disambiguating Neural Linguistic Steganography [66.30965740387047]
  サブワードに基づく言語モデルを使用する際に生じるセグメンテーションの曖昧さ問題は、時にはデコード障害を引き起こす。 そこで我々はSyncPoolという,セグメンテーションのあいまいさ問題に効果的に対処する,セキュアな曖昧さ回避手法を提案する。 SyncPoolは、候補プールのサイズやトークンの分布を変えないため、確実に安全な言語ステガノグラフィー手法に適用できる。
  論文  参考訳（メタデータ） (2024-03-26T09:25:57Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。 セキュアマルチパーティ計算(MPC)を特に対象とする。 MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
  論文  参考訳（メタデータ） (2024-03-08T02:02:24Z)
• A Modular Approach to Unclonable Cryptography [4.336971448707467]
  本稿では,不規則な句読解難読解法(UPO)を提案する。 我々は、多くのプリミティブのモジュラー構造(そして間違いなく単純な)を、制限不能な暗号で提示する。 暗号化機能は、この機能がセキュリティの概念を満たす限り、コピープロテクト可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-20T16:22:52Z)
• CryptoBap: A Binary Analysis Platform for Cryptographic Protocols [6.514727189942011]
  暗号プロトコルの弱い秘密と認証を検証するプラットフォームであるCryptoBapを紹介する。 まずプロトコルのバイナリを中間表現に変換し、次に暗号対応のシンボル実行を実行する。 提案手法の健全性を実証し,CryptoBapを用いて,おもちゃの例から実世界のプロトコルまで,複数のケーススタディを検証した。
  論文  参考訳（メタデータ） (2023-08-28T09:41:45Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。 主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。 理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
  論文  参考訳（メタデータ） (2023-05-20T11:26:51Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)
• Revocable Cryptography from Learning with Errors [61.470151825577034]
  我々は、量子力学の非閉鎖原理に基づいて、キー呼び出し機能を備えた暗号スキームを設計する。 我々は、シークレットキーが量子状態として表現されるスキームを、シークレットキーが一度ユーザから取り消されたら、それらが以前と同じ機能を実行する能力を持たないことを保証して検討する。
  論文  参考訳（メタデータ） (2023-02-28T18:58:11Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• 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)

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

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