文章基本信息

标题：形式手法を用いたディジタル署名システムの安全性評価
本地全文：下载
作者：宮崎邦彦 ; David BASIN ; 來間啓伸等
期刊名称：コンピュータソフトウェア
印刷版ISSN：0289-6540
出版年度：2005
卷号：22
期号：2
页码：2_74-2_84
DOI：10.11309/jssst.22.2_74
出版社：Japan Society for Software Science and Technology
摘要：
本稿では，ディジタル署名システムのモデル化と検証に形式手法を用いたケーススタディについて述べる．われわれは，複数OS (operating system)を1台の計算機上に共存させるDARMAと呼ばれるソフトウェア上に実装されたディジタル署名システムの安全性を検証した．具体的には，対象システムをPROMELA (PROcess MEta LAnguage)を用いてモデル化し，さらに，SPINモデルチェッカを用いてデータの完全性について検証を行った．以下では，われわれのモデル化のアプローチとその安全性検証から得られたメリットについて述べる．