CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 18: ソフトウェア更新システムプロトコルのBAN Logicによる安全性検証


実施年度2005
概要 BAN logic は認証プロトコルの分析を行うために与えられた論理の形式体系 である. 本研究では, BAN logic を食品産業向け商品処理装置のために開発 中であるソフトウエア更新システムのプロトコルに適用し, その安全性を検 証した. まず, 与えられたプロトコルについて, その仕様から帰結できる性質を示した. 次に, 通信経路上に悪意のある振る舞いを持つ主体が存在しても「商品処理装 置は最新版の更新プログラムを受信するか, もしくはエラー通知を受信(送信) する」という性質を満たすよう, 最初のプロトコルを変更することによって得 られた2つのプロトコルを与えた.
担当者 吉田聡, 山形頼之
班名 フィールドワーク3班
寄与 株式会社イシダ
関連する事例

題材

領域 プロトコル
題材の詳細
・検証対象は, 工場内のネットワーク中継装置を介して, 工場内の商品処理装
置と管理サーバを接続し, 更新ソフトウェアを管理サーバから商品処理装置へ
ダウンロードするシステムのプロトコルである.

・プロトコルにおけるエージェントは, 商品処理装置, 中継装置, 管理サーバ,
コード署名局の4つ. 商品処理装置と管理サーバの間の要求やファイルの送信
は中継装置を経由して行われる.

・署名はコード署名局と商品処理装置が行う. その署名はそれぞれの公開鍵を
用いて行われる.

・コード署名局は, 管理サーバが商品処理装置に向けて送信するすべてのファ
イルに予め署名を行う.

・送受信を行うエージェントの間には共通鍵あり, 送受信の際, 共通鍵による
暗号化と複合化を行う.

・プロトコルの概要は次の通り:
i. 商品処理装置が, INFファイルと呼ばれる, 自身の情報とすでにインス
トールされているソフトウェアの情報を記載したファイルを公開鍵による署
名を行い, 中継装置に送信する.
ii. そのINFファイルを中継装置はそのまま管理サーバに送信する.
iii.管理サーバは受信したINFファイルの署名を確認することによって, INF
ファイルの送信者を知る. その後, 管理サーバは更新すべきソフトウェアの
有無についての情報を中継装置に送信する.
iv. 中継装置はその更新についての情報を商品処理装置に送信する.
v. ソフトウェアの更新がある場合, 中継装置は管理サーバに, まず,
新しいソフトウェアの情報が記載された新しいINFファイルを送信するよう要
求を出す.
vi. 管理サーバはコード署名局によって署名された新しいINFファイルを中
継処理装置に送信する.
vii. 新しいINFファイルを中継装置は受信した後, 管理サーバに更新ソ
フトウェアの送信の要求を出す.
viii.管理サーバは更新ファイルを中継装置に送信する.
ix. 商品処理装置は中継装置に新しいINFファイルの送信を要求する.
x. 中継装置はすでに管理サーバから受信した新しいINFファイルを商品処理
装置に送信する.
xi. 新しいINFファイルの受信後, 中継装置は商品処理装置に更新ソフ
トウェアを送信する.
形態 仕様書
言語 日本語
規模 対象が持つ性質を示すBAN Logicの論理式は10個. そこから, 改善案を示すために与えた仮定を表すBAN Logicの論理式は3個.
題材の情報源 株式会社イシダ

検証のデータ

目的
設計途中に定理証明を導入する方法を検討する.
検証内容
検証項目として、
「商品処理装置は最新版の更新プログラムを受信するか, もしくはエラー通
知を受信(送信)する」
を置き、最初に与えられたプロトコルがこれを満たすか否かを明らかにし,
満たさない場合は満たすための変更案を示すことを目標とした.
結果
1.最初に与えられたプロトコルが次の性質を持つことを示した:
・商品処理装置が受信したファイル(更新プログラム, 新INFファイル)は
コード署名局を経て送信されたものであると, 商品処理装置側からも信頼で
きる.
・管理サーバが受信した現行INFファイルは商品処理装置から送信されたもの
であると, 管理サーバ側からも信頼できる.

2.「商品処理装置側から見て, 更新したプログラムが実際に管理サーバが持
つ最新版であると信頼できる」という性質について, 最初に与えられたプロ
トコルの仕様からは導き出せないことを示した.
例えば, 中継装置が悪意を持っていて, 商品処理装置から送信されたINFファ
イルを途中にある中継装置が書き換えたり, また管理サーバから送信された
更新プログラムを古い更新プログラムにすり替えたりした場合を最初に与えら
れたプロトコルではは検出できない.

3. 上記2の脆弱性を解消するため, 次の改善案を示した.
・ 管理サーバが常に信頼できる場合:
商品処理装置から現行INFファイルを送信する際, 品処理装置は新たにナン
スを生成し, それも加えて送信する. そのとき, 商品処理装置はそれら2つ
を合わせて署名する. 管理サーバは商品処理装置から送られたナンスと新INF
ファイルに対して合わせて署名し, それらを送信する. また, 更新プログラ
ムについても同様に, その商品処理装置からのナンスと合わせて署名し送信
する.
商品処理装置は, 受信したINFファイルや更新プログラムに添えられているナ
ンスが, 自身が最近生成したものであるかどうかを確認し, 自身の最近生成し
たナンスであれば, それらINFファイルや更新プログラムは最新のものであ
ると商品処理装置は信頼できる.
・管理サーバが信頼できない場合:
コード署名局が商品処理装置ごとの要求に対応すると仮定. 商品処理装置か
ら現行INFファイルを送信する際, 商品処理装置は新たにナンスを生成し, そ
れも加えて送信する. そのとき, 商品処理装置はそれら2つを合わせて署名する.
コード署名局は商品処理装置から送られたナンスと新INFファイルを合わせて
署名する. また, 更新プログラムもそのナンスと合わせて署名する.
商品処理装置は受信したINFファイルや更新プログラムに添えられているナン
スが自身が最近生成したものかどうかを検証し, 自身が最近生成したナンス
であれば, それらINFファイルや更新プログラムは最新のものであると商品処
理装置は信頼できる.

検証手法 定理証明
モデル化法 ドキュメントからの手動.
使用ツール なし. 人手による計算.
スケジュール、
労力、時間など
10日×2人
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2007-006, ソフトウェア更新システムプロトコルのBAN Logic による安全性検証(Preliminary Version), 吉田聡, 山形頼之, http://unit.aist.go.jp/cvs/tr-data/PS2007-006.pdf
論文発表
口頭発表
知的財産
その他

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.