文献

J-GLOBAL ID：202002289661093595   整理番号：20A0777630

識別不能性に基づく計算完全記号攻撃者のための検証法【JST・京大機械翻訳】

Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability

著者 (4件)： Bana Gergei (University of Missouri, USA and University of Luxembourg, Luxembourg) ,  Chadha Rohit (University of Missouri, USA) ,  Eeralla Ajay Kumar (University of Missouri, USA) ,  Okada Mitsuhiro (Keio University, Tokyo, Japan)
資料名： ACM Transactions on Computational Logic  (ACM Transactions on Computational Logic)
巻： 21  号： 1  ページ： 1-44  発行年： 2019年 
JST資料番号： A1264A  ISSN： 1529-3785  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 近年,記号攻撃者の利益と無条件健全性の利点を組み合わせることを目的として,セキュリティプロトコルを検証するための新しいアプローチが開発されている:BanaとComon(BC)[8]の計算的に完全な記号攻撃者の技術。本論文では,この技術の実際のブレークスルーが,ここで紹介する拡張により,非識別可能性に対するそのバージョンの最近の導入であることを論じた。ここでは,標準的な計算セキュリティ概念が直接的なものであり,また,プロトコルの等価性特性だけでなく,トレース特性の検証にも有効に使用できる。最初に,いくつかの新しい公理を導入することにより,この新しいバージョンのコア要素を完全に開発した。著者らは,最初に簡単な例に関する導入された公理のパワーと多様な使用を例示した。決定的Diffie-Hellman特性を表す公理を導入した。Diffie-Hellman鍵交換を,その最も単純な形式と認証バージョンの両方で解析した。多重セッションに対するDiffie-Hellman鍵交換プロトコルの実ランダム秘密の計算的に健全な検証を提供し,DDH仮定以外の計算実行に制約を与えなかった。また,ディジタル署名に対するUF-CMAの仮定を用いて,状態から局へのプロトコルの単純化版に対する認証を示した。最後に,IND-CPA,IND-CCA1,およびIND-CCA2セキュリティ特性を公理化し,それらの利用を例示した。著者らは,対話型定理証明器Coqにおける公理的システムを定式化し,Diffie-Hellmanの種々の補助定理とセキュリティ特性の証明を機械的にチェックした。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 計算モデル ,  *公理 ,  健全性 ,  定理証明 ,  簡素化 ,  認証 ,  等価性 ,  定式化 ,  セキュリティ ,  多重化 ,  ディジタル署名 ,  公理化 ,  セキュリティプロトコル ,  改変
準シソーラス用語： *攻撃者 , 【Automatic Indexing@JST】

著者キーワード (6件)： 認証 ,  DOLEV-YAOモデル ,  計算モデル ,  計算健全性 ,  一次論理 ,  秘密

分類 (3件)： 符号理論  (ND02030R) ,  データ保護  (JD01020V) ,  計算機網  (JC03000K)

タイトルに関連する用語 (5件)： 識別 ,  計算 ,  記号 ,  攻撃者 ,  検証