言語と計算の科学

次世代webの安全性がより確かなものに

~フォーマルメソッドによるQUIC・TLS1.3の検証~

概要

インターネット上の通信の安全性は、認証や暗号化の方法を定めたセキュリティ・プロトコルに従って守られています。しかし近年その欠陥がたびたび発見されています。対策までの間は危険な状態が続くとともに, 対策には多大なコストを要します。本研究では、数理論理学に基づくフォーマルメソッドを利用し、プロトコルが与えられた安全性を満たすかどうかを計算機を用いて厳密に検査することで、プロトコルが利用される前に欠陥を発見します。特に、次世代web認証・暗号化プロトコルTLS1.3の安全性を確認し、さらに、Googleによって策定されたweb認証・暗号化プロトコルQUICが従来研究で証明された安全性を満たさないことを発見しました。

当日の様子

ポスター


ポスターの画像をクリックすると、PDFファイルが開きます。

展示担当者

櫻田 英樹
櫻田 英樹
メディア情報研究部
真野 健
真野 健
メディア情報研究部
塚田 恭章
塚田 恭章
メディア情報研究部