論文の概要: DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
- arxiv url: http://arxiv.org/abs/2211.03225v2
- Date: Mon, 11 Mar 2024 18:06:10 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-17 17:20:31.186606
- Title: DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice
- Title（参考訳）: DeepSec: セキュリティプロトコルの等価性の決定 -- 理論とプラクティスの改善
- Authors: Vincent Cheval, Steve Kremer, Itsaka Rakotonirina,
- Abstract要約: 我々はこの検証問題の理論と実践に貢献する。
静的同値、トレース同値およびラベル付き二相性のための新しい複雑性結果を確立する。
我々の手順は、多種多様な暗号プリミティブに対して、トレース同値とラベル付き二相性を決定する最初の方法である。
- 参考スコア（独自算出の注目度）: 8.735998284944436
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Automated verification has become an essential part in the security evaluation of cryptographic protocols. In this context privacy-type properties are often modelled by indistinguishability statements, expressed as behavioural equivalences in a process calculus. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of protocol sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We also implemented the procedure in a new tool, DeepSec. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
- Abstract（参考訳）: 自動検証は暗号プロトコルのセキュリティ評価において欠かせない部分となっている。
この文脈では、プライバシ型プロパティは、しばしばプロセス計算における振る舞いの等価性として表される不明瞭性ステートメントによってモデル化される。
本稿では,この検証問題の理論と実践に貢献する。
我々は,静的同値性,トレース同値性,ラベル付き二相性のための新しい複雑性結果を確立し,有界なプロトコルセッションの場合のこれらの同値性の決定手順を提供する。
我々の手順は、多種多様な暗号プリミティブに対して、トレース同値とラベル付き二相性を決定する最初の方法である。
また、新しいツールであるDeepSecにもプロシージャを実装しました。
我々は、他の類似ツールよりもはるかに効率的であると同時に、分析可能なプロトコルの範囲を高くすることを示した。
関連論文リスト
- DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。
セキュアマルチパーティ計算(MPC)を特に対象とする。
MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
論文 参考訳（メタデータ） (2024-03-08T02:02:24Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
対象中心のペトリネットが一対多の関係を捉える能力と,その同一性に基づいたオブジェクトの比較と同期を行う識別子を持つペトリネットの能力を組み合わせた,新たな形式主義を提案する。
我々は、満足度変調理論(SMT)の符号化に基づく、そのようなネットに対する適合性チェック手法を提案する。
論文 参考訳（メタデータ） (2023-12-13T21:53:32Z) - Test Case Recommendations with Distributed Representation of Code
Syntactic Features [2.225268436173329]
本稿では,ソースコード手法とテストケースの構造的・意味的特性を利用する自動手法を提案する。
提案するアプローチは、当初、メソッドレベルのソースコードとユニットテストを分散表現に変換するためにニューラルネットワークをトレーニングする。
このモデルは、メソッドの埋め込みと以前に組み込まれたトレーニングインスタンスのコサイン類似性を計算します。
論文 参考訳（メタデータ） (2023-10-04T21:42:01Z) - Object Type Clustering using Markov Directly-Follow Multigraph in
Object-Centric Process Mining [2.3351527694849574]
本稿では,Markov Directly-Follow Multigraphに基づくクラスタ類似のケース概念に対する新しいアプローチを提案する。
しきい値チューニングアルゴリズムは、異なるレベルの類似性に基づいて発見できる異なるクラスタの集合を特定するためにも定義される。
論文 参考訳（メタデータ） (2022-06-22T12:36:46Z) - Data post-processing for the one-way heterodyne protocol under
composable finite-size security [62.997667081978825]
本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。
ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。
これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
論文 参考訳（メタデータ） (2022-05-20T12:37:09Z) - FineDiving: A Fine-grained Dataset for Procedure-aware Action Quality
Assessment [93.09267863425492]
競争力のあるスポーツビデオにおける行動の高レベル意味論と内部時間構造の両方を理解することが、予測を正確かつ解釈可能なものにする鍵である、と我々は主張する。
本研究では,多様なダイビングイベントに対して,アクションプロシージャに関する詳細なアノテーションを付加した,ファインディビングと呼ばれる詳細なデータセットを構築した。
論文 参考訳（メタデータ） (2022-04-07T17:59:32Z) - Benchmarking Deep Models for Salient Object Detection [67.07247772280212]
汎用SALOD(General SALient Object Detection)ベンチマークを構築し,複数のSOD手法の総合的な比較を行った。
以上の実験では、既存の損失関数は、通常いくつかの指標に特化しているが、他の指標には劣る結果が報告されている。
我々は,深層ネットワークに画素レベルと画像レベルの両方の監視信号を統合することにより,より識別的な特徴を学習するためのエッジ・アウェア・ロス(EA)を提案する。
論文 参考訳（メタデータ） (2022-02-07T03:43:16Z) - Quantum anonymous veto: A set of new protocols [0.41998444721319217]
本稿では,異なる種類の量子リソースに基づく量子匿名拒否(QAV)プロトコルを提案する。
提案手法は有効なQAV方式のすべての要求に対して解析される。
確率的QAVスキームの正しさと頑健さのトレードオフが観察された。
論文 参考訳（メタデータ） (2021-09-13T18:56:09Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - Efficient Conformance Checking using Approximate Alignment Computation
with Tandem Repeats [0.03222802562733786]
コンフォーマンスチェックは、期待されるプロセスの振る舞いをキャプチャするプロセスモデルと、観測された振る舞いを記録する対応するイベントログの違いを発見し、記述することを目的としている。
アライメントは、イベントログ内のトレースと、対応するプロセスモデルの最も近い実行トレースの間の距離を計算するための確立されたテクニックである。
本稿では,前処理と後処理を併用してトレースの長さを圧縮し,アライメントコストを再計算する手法を提案する。
論文 参考訳（メタデータ） (2020-04-02T03:50:32Z) - Certified Robustness to Label-Flipping Attacks via Randomized Smoothing [105.91827623768724]
機械学習アルゴリズムは、データ中毒攻撃の影響を受けやすい。
任意の関数に対するランダム化スムージングの統一的なビューを示す。
本稿では,一般的なデータ中毒攻撃に対して,ポイントワイズで確実に堅牢な分類器を構築するための新しい戦略を提案する。
論文 参考訳（メタデータ） (2020-02-07T21:28:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。