文献

J-GLOBAL ID：202002224426480297   整理番号：20A2554213

LoRaWAN鍵確立の広範なセキュリティ検証:セキュリティとパッチ【JST・京大機械翻訳】

Extensive Security Verification of the LoRaWAN Key-Establishment: Insecurities & Patches

著者 (4件)： Wesemeyer Stephan (University of Surrey, Surrey Centre for Cyber Security,Guildford,UK) ,  Boureanu Ioana (University of Surrey, Surrey Centre for Cyber Security,Guildford,UK) ,  Smith Zach (University of Luxembourg,Esch-sur-Alzette,Luxembourg) ,  Treharne Helen (University of Surrey, Surrey Centre for Cyber Security,Guildford,UK)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2020  号： EuroS&P  ページ： 425-444  発行年： 2020年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： LoRaWAN(低電力ワイドネットワーク)は,アプリケーションレベルIoT(モノのインターネット)の主な仕様である。2017年10月に発表された現在のバージョンは,LoRaWAN1.1であり,その1.0の前駆体は,PyCom LoRaトランシーバのような商用装置によって支持された主な仕様である。LoRaWANプロトコルのセキュリティに対する事前(半)形式研究は,特にLo-RaWAN1.1に対して不足している。さらに,これらの少数の中で,LoRaWANの[9]と検証ツールへの現在の符号化は,LoRaWANプロトコルの非常に単純化されたバージョンに不幸にも依存し,実際に結果の関連性を過小評価する。本論文では,これらのギャップのいくつかを埋める。LoRaWAN 1.1に見える最も最近の暗号指向研究[5]を手短に議論し,著者らの真の焦点は,自動化ツールの中で機械化されたLoRaWANのセキュリティと正当性の形式的解析を生成することである。この目的のために,最先端の証明器,タマリンを用いた。重要なことに,著者らのタマリンモデルはLoRaWAN仕様の忠実で正確なレンダリングである。例えば,LoRaWAN 1.1に新たに導入された,また「古典的」であるが,LoRaWAN 1.0における短いドメイン非コード,およびこれらに関する推奨事項を新たに導入した,スポーク非発生メカニズムをモデル化した。デバイスコンミッションとアプリケーションレベルトラフィックに関する小部分を含むが,著者らは主にLoRaWANのJoin手順を精査し,仕様のバージョン1.1に焦点を合わせるが,Lo-RaWAN1.0の解析も含めた。この目的のために,著者らは,様々なチャネル(例えば,安全/不安全)およびエンティティ上に置かれた信頼のレベル(例えば,正直/崩壊ネットワークサーバ)に関して作られた,Dolev-Yao攻撃者に作用する3つのますます強い脅威モデルを考察した。重要なことは,これらの脅威モデルの1つがLoRaWAN仕様と正確に合致しているが,まだ,まだ攻撃に至っていない。示した攻撃に対応して,著者らは,現在のバージョンとできるだけ逆互換性であるLoRaWAN1.1 Join手順の最小パッチを提案した。上述の最強の脅威モデルにおいて,このパッチセキュアを分析し,証明した。本研究は,LoRa Allianceに責任があり,LoRa Allianceのセキュリティワーキンググループと,著者らの発見の見地から,LoRaWAN 1.1仕様の明瞭度を改善するために,また,将来および現在の仕様書込みのフィードバックループの一部として,形式的解析を用いることによって,著者らは,liaIsingした。Copyright 2020 The Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 自動化 ,  簡素化 ,  機械化 ,  互換性 ,  明瞭度 ,  送受信機 ,  *応用プログラム ,  前駆体 ,  暗号 ,  チャネル ,  レンダリング ,  セキュリティ
準シソーラス用語： フィードバックループ ,  モノのインターネット ,  *鍵確立 , 【Automatic Indexing@JST】

分類 (1件)： 図形・画像処理一般  (JE04010I)

タイトルに関連する用語 (5件)： LoRaWAN ,  鍵確立 ,  セキュリティ ,  検証 ,  パッチ