論文の概要: Cryptis: Cryptographic Reasoning in Separation Logic

• arxiv url: http://arxiv.org/abs/2502.21156v1
• Date: Fri, 28 Feb 2025 15:33:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-03 13:40:08.875121
• Title: Cryptis: Cryptographic Reasoning in Separation Logic
• Title（参考訳）: Cryptis: 分離論理における暗号推論
• Authors: Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi,
• Abstract要約: 我々は,Iris分離論理の拡張であるCryptisを導入し,暗号の記号モデルを用いて暗号部品の検証を行う。 分離論理と暗号推論の組み合わせにより、プロトコルの正当性を証明し、後にこの結果を再利用して、プロトコルに依存するより大きなシステムを検証することができる。
• 参考スコア（独自算出の注目度）: 6.965792280784777
• License:
• Abstract: We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq.
• Abstract（参考訳）: 我々は,Iris分離論理の拡張であるCryptisを導入し,暗号の記号モデルを用いて暗号部品の検証を行う。 分離論理と暗号推論の組み合わせにより、プロトコルの正当性を証明し、後にこの結果を再利用して、プロトコルに依存するより大きなシステムを検証することができる。 この統合を可能にするため,ネットワーク内のエージェントがシステムリソースの使用に合意できる認証プロトコルの新たな仕様を提案する。 我々は,これらの認証プロトコルを用いてクライアントに接続する各種認証プロトコルとキーバリューストアサーバを検証し,そのアプローチを評価する。 私たちの結果はCoqで形式化されています。

関連論文リスト

• Thetacrypt: A Distributed Service for Threshold Cryptography [0.0]
  Thetacryptは多くのしきい値スキームをひとつの言語に統合するための汎用ライブラリである。 しきい値暗号を使って分散システムを簡単に構築する方法を提供する。 このライブラリには、暗号、シグネチャ、ランダムネス生成にまたがる6つの暗号スキームが含まれている。
  論文  参考訳（メタデータ） (2025-02-05T15:03:59Z)
• Cryptanalysis via Machine Learning Based Information Theoretic Metrics [58.96805474751668]
  本稿では,機械学習アルゴリズムの新たな2つの応用法を提案する。 これらのアルゴリズムは、監査設定で容易に適用でき、暗号システムの堅牢性を評価することができる。 本稿では,DES,RSA,AES ECBなど,IND-CPAの安全でない暗号化スキームを高精度に識別する。
  論文  参考訳（メタデータ） (2025-01-25T04:53:36Z)
• Secure Semantic Communication With Homomorphic Encryption [52.5344514499035]
  本稿では,SemCom に準同型暗号を適用する可能性について検討する。 タスク指向のSemComスキームを提案する。
  論文  参考訳（メタデータ） (2025-01-17T13:26:14Z)
• 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)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
  論文  参考訳（メタデータ） (2024-05-09T19:57:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• LpiCT: A logic security analysis framework for protocols [1.4852249222037588]
  本稿では,論理規則と証明,バイナリツリー,KMPアルゴリズムを導入し,論理セキュリティ解析フレームワークとアルゴリズムを新たに拡張する。 実験結果から,新たな拡張理論,論理セキュリティ分析フレームワーク,アルゴリズムが,暗号プロトコルの設計と実装に論理的欠陥があるかどうかを効果的に解析できることが示唆された。
  論文  参考訳（メタデータ） (2023-11-01T12:06:47Z)
• A Security Verification Framework of Cryptographic Protocols Using Machine Learning [0.0]
  機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。 ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。 提案手法を実用的な暗号プロトコルの検証に適用して評価する。
  論文  参考訳（メタデータ） (2023-04-26T02:37:43Z)
• Secure access system using signature verification over tablet PC [62.21072852729544]
  我々は,シグネチャ検証を用いたWebベースのセキュアアクセスのための,高度に汎用的でスケーラブルなプロトタイプについて述べる。 提案アーキテクチャは,様々な種類のセンサや大規模データベースで動作するように容易に拡張することができる。
  論文  参考訳（メタデータ） (2023-01-11T11:05:47Z)

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

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