論文の概要: LpiCT: A logic security analysis framework for protocols
- arxiv url: http://arxiv.org/abs/2312.02171v1
- Date: Wed, 1 Nov 2023 12:06:47 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-25 12:57:08.194322
- Title: LpiCT: A logic security analysis framework for protocols
- Title（参考訳）: LpiCT:プロトコルのためのロジックセキュリティ分析フレームワーク
- Authors: Fusheng Wu, Jinhui Liu, Yanbing Li, Mingtao Ni,
- Abstract要約: 本稿では,論理規則と証明,バイナリツリー,KMPアルゴリズムを導入し,論理セキュリティ解析フレームワークとアルゴリズムを新たに拡張する。
実験結果から,新たな拡張理論,論理セキュリティ分析フレームワーク,アルゴリズムが,暗号プロトコルの設計と実装に論理的欠陥があるかどうかを効果的に解析できることが示唆された。
- 参考スコア（独自算出の注目度）: 1.4852249222037588
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The pi calculus is a basic theory of mobile communication based on the notion of interaction, which, aimed at analyzing and modelling the behaviors of communication process in communicating and mobile systems, is widely applied to the security analysis of cryptographic protocol's design and implementation. But the pi calculus does not provide perfect logic security analysis, so the logic flaws in the design and the implementation of a cryptographic protocol can not be discovered in time. The aim is to analyze whether there are logic flaws in the design and the implementation of a cryptographic protocol, so as to ensure the security of the cryptographic protocol when it is encoded into a software and implemented. This paper introduces logic rules and proofs, binary tree and the KMP algorithm, and proposes a new extension the pi calculus theory, a logic security analysis framework and an algorithm. This paper presents the logic security proof and analysis of TLS1.3 protocol's interactional implementation process. Empirical results show that the new extension theory, the logic security analysis framework and the algorithm can effectively analyze whether there are logic flaws in the design and the implementation of a cryptographic protocol. The security of cryptographic protocols depends not only on cryptographic primitives, but also on the coding of cryptographic protocols and the environment in which they are implemented. The security analysis framework of cryptographic protocol implementation proposed in this paper can ensure the security of protocol implementation.
- Abstract（参考訳）: 通信およびモバイルシステムにおける通信プロセスの動作を分析しモデル化することを目的としたインタラクションの概念に基づく移動通信の基本理論であり,暗号プロトコルの設計と実装のセキュリティ解析に広く応用されている。
しかし、pi計算は完全なロジックセキュリティ解析を提供していないため、設計におけるロジックの欠陥や暗号プロトコルの実装は時間内には発見できない。
本研究の目的は,暗号プロトコルの設計や実装に論理的欠陥があるかどうかを解析し,ソフトウェアにコード化して実装する際の暗号プロトコルのセキュリティを確保することである。
本稿では,論理規則と証明,バイナリツリー,KMPアルゴリズムを導入し,論理セキュリティ解析フレームワークとアルゴリズムを新たに拡張する。
本稿では,TLS1.3プロトコルの相互運用プロセスの論理セキュリティ証明と解析について述べる。
実験結果から,新たな拡張理論,論理セキュリティ分析フレームワーク,アルゴリズムが,暗号プロトコルの設計と実装に論理的欠陥があるかどうかを効果的に解析できることが示唆された。
暗号プロトコルのセキュリティは、暗号プリミティブだけでなく、暗号プロトコルのコーディングや実装環境にも依存する。
本稿では,暗号プロトコル実装のセキュリティ分析フレームワークを用いて,プロトコル実装のセキュリティを確保する。
関連論文リスト
- CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。
私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
論文 参考訳（メタデータ） (2024-11-20T14:16:55Z) - DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。
セキュアマルチパーティ計算(MPC)を特に対象とする。
MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
論文 参考訳（メタデータ） (2024-03-08T02:02:24Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。
このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。
我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
論文 参考訳（メタデータ） (2024-01-06T02:57:44Z) - An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳（メタデータ） (2023-12-08T09:32:26Z) - SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
本稿では,SOCIの性能を大幅に向上させるSOCI+を提案する。
SOCI+は、暗号プリミティブとして、高速な暗号化と復号化を備えた(2, 2)ホールドのPaillier暗号システムを採用している。
実験の結果,SOCI+は計算効率が最大5.4倍,通信オーバヘッドが40%少ないことがわかった。
論文 参考訳（メタデータ） (2023-09-27T05:19:32Z) - A Security Verification Framework of Cryptographic Protocols Using
Machine Learning [0.0]
機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。
ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。
提案手法を実用的な暗号プロトコルの検証に適用して評価する。
論文 参考訳（メタデータ） (2023-04-26T02:37:43Z) - Evidential Transactions with Cyberlogic [0.6091702876917281]
Cyberlogicは、デジタルトランザクションの構築と分析のための論理的基盤である。
1)公開鍵は認証に対応し,(2)トランザクションは分散論理プログラムとして指定され,(3)検証された証拠は分散証明探索によって収集される。
論文 参考訳（メタデータ） (2023-03-20T10:18:43Z) - Towards Semantic Communication Protocols: A Probabilistic Logic
Perspective [69.68769942563812]
我々は,NPMを確率論理型言語ProbLogで記述された解釈可能なシンボルグラフに変換することによって構築された意味プロトコルモデル(SPM)を提案する。
その解釈性とメモリ効率を利用して、衝突回避のためのSPM再構成などのいくつかの応用を実演する。
論文 参考訳（メタデータ） (2022-07-08T14:19:36Z) - Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
本稿では,プラットフォームに依存しない論理ゲート定義の必要性から,普遍的なフォールトトレラント論理の枠組みを提案する。
資源オーバーヘッドを改善するユニバーサル論理の新しいスキームについて検討する。
境界のない計算に好適な論理誤差率を動機として,新しい計算手法を提案する。
論文 参考訳（メタデータ） (2021-12-22T19:00:03Z) - Security analysis method for practical quantum key distribution with
arbitrary encoding schemes [7.321809883860193]
符号化方式の制約のないセキュリティ解析手法を提案する。
ソース欠陥と高次元非対称プロトコルを解析することにより,その能力を説明する。
我々の研究は、実用的なQKDのセキュリティ分析の基準となる可能性を持っている。
論文 参考訳（メタデータ） (2021-09-10T09:53:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。