文献

J-GLOBAL ID：202002291509952431   整理番号：20A1863967

W3Cウェブ認証プロトコルの形式的検証【JST・京大機械翻訳】

Formal verification of the W3C web authentication protocol

著者 (2件)： Guirat Iness Ben (INSAT, Tunis, Tunisia) ,  Halpin Harry (Inria, Paris, France)
資料名： ACM Proceedings  (ACM Proceedings)
号： HoTSoS ’18  ページ： 1-10  発行年： 2018年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： セキュリティの科学は,プロトコルの正式な検証を通して強固な基礎に設定できる。新しいプロトコルは,セキュリティ欠陥のために機械化された方法で検証されるそれらの設計を持ち,プロトコル設計を中性方式で科学的に比較できる。これらの技法がTLS 1.2のようなプロトコルにおいて重大な欠陥を発見し,現在TLS 1.3のようなプロトコルを再設計するために使用されていることを考えると,W3C Web認証APIのような新しいプロトコルを解析するために形式的検証がいかに使用できるかを示した。W3C Web認証を形式的検証言語ProVerifでモデル化し,プロトコル自体が安全であることを示した。しかし,同じ起源政策に関して与えられたW3C Web認証のプライバシー特性を検証する試みによって,形式的検証の境界を伸ばした。ProVerifを用いて,仕様における更なる必須要件なしで,主張プライバシー特性が保持されないことを示した。次に,形式的検証を標準に統合できるか,そして,W3C Web認証のプライバシー特性のさらなる発展について概説した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 機械化 ,  言語 ,  プライバシー ,  再設計 ,  ロバスト性 ,  セキュリティ ,  *Web【情報システム】 ,  *認証
準シソーラス用語： 証明書 ,  形式的検証 ,  *認証プロトコル ,  プロトコル設計 , 【Automatic Indexing@JST】

著者キーワード (5件)： W3Cウェブ認証 ,  認証 ,  形式的検証 ,  証明書 ,  セキュリティの科学

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

タイトルに関連する用語 (4件)： W3C ,  ウェブ ,  認証プロトコル ,  形式的検証