文献

J-GLOBAL ID：202002272790014050   整理番号：20A2694142

TEEベースプロトコルの系統的解析のための記号モデル【JST・京大機械翻訳】

A Symbolic Model for Systematically Analyzing TEE-Based Protocols

著者 (6件)： Xu Shiwei (College of Informatics, Huazhong Agricultural University, Wuhan, People’s Republic of China) ,  Zhao Yizhi (College of Informatics, Huazhong Agricultural University, Wuhan, People’s Republic of China) ,  Ren Zhengwei (School of Computer Science and Technology, Wuhan University of Science and Technology, Wuhan, People’s Republic of China) ,  Wu Lingjuan (College of Informatics, Huazhong Agricultural University, Wuhan, People’s Republic of China) ,  Tong Yan (College of Science, Huazhong Agricultural University, Wuhan, People’s Republic of China) ,  Zhang Huanguo (College of Cyber Science and Engineering, Wuhan University, Wuhan, People’s Republic of China)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12282  ページ： 126-144  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 様々なプロトコルのための孤立貯蔵および計算環境を提供するためのアプローチとして,信頼された実行環境(TEE)が広く使われており,従って,TEEのセキュリティ特徴は,これらのプロトコルを設計する方法を決定する。しかし,実際には,新しいTEEベースプロトコルが経験的に設計され,実際の脅威モデルに対する包括的な解析の欠如が脆弱性と攻撃を容易にもたらす。通信チャネルまたは安全なエンクラブに焦点を当てたほとんどの過去の研究とは異なり,著者らは,Tamarinによって瞬時化されたスケーラブルなマルチセット書き込みモデリングフレームワークと共に,ネットワークとTEEベースのプラットフォームの両方からの攻撃を考慮した詳細な脅威モデルを含む,TEEベースのプロトコルのための形式的モデルを提示する。提案した脅威モデルと形式に基づいて,著者らは,脅威のすべての組合せを考慮して,関連オフラインとWebベースのプロトコルを系統的に自動的に分析するために,タマリンを使用した。結果と比較は,TEEベースのプラットフォームから継承されたプロトコルの長所と弱点を強調する。さらに,著者らは従来の脅威モデルの下で見つけるのが難しいいくつかの脆弱性を捕えて,対応する固定を提案した。Copyright Springer Nature Switzerland AG 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： ネットワーク ,  通信チャネル ,  セキュリティ ,  *Web【情報システム】
準シソーラス用語： 多重集合 ,  脆弱性 ,  セキュリティプロトコル ,  実行環境 ,  オフライン , 【Automatic Indexing@JST】

著者キーワード (4件)： 信頼実行環境 ,  セキュリティプロトコル ,  形式的検証 ,  セキュリティ解析

分類 (2件)： データ保護  (JD01020V) ,  計算機網  (JC03000K)

タイトルに関連する用語 (6件)： TEE ,  プロトコル ,  系統 ,  解析 ,  記号 ,  モデル