STSプロトコルの形式化と検証によるCafeOBJとCoqの比較

摘要

形式手法により検証を行う技法は広く研究され，これまでに多くの方法が提案されてきた．しかし，方法の提案や実例を扱う研究に比べ，その比較を扱う研究はあまり行われておらず，その結果，形式手法を用いる際のガイドラインがないという問題点が存在する．本稿では，セキュリティプロトコルの一つであるSTSプロトコルを例題として取り上げ，異なる二つの形式手法として，CafbOBJを用いる方法とCoqを用いる方法の双方で安全性等の検証を行う。 この具体例を通して，双方によるシステムの形式化および検証の，手法についての比較を行い，長所·短所を明らかにする．