公立鳥取環境大学紀要
第14号（2016．３）pp.95-103〔報告〕

ソフトウェア更新システムプロトコルの様相論理 S4に基づく検証

A verification based on modal logic S4 of the software update system protocol

吉田聡

YOSHIDA Satoru

要旨：食品産業向け商品処理装置のために開発されていたあるソフトウェア更新システムのプロトコルに対して BAN 論理に基づく定理証明と LTL モデル検査によって行われた検証事例が知られている。本稿
では、その事例と同様の検証を様相論理 S4に基づいて行った事例を報告する。
【キーワード】定理証明、モデル検査、様相論理、S4
Abstract：There is a formal verification case study of a certain software update system protocol, based on BAN logic theorem proving and LTL model checking. This article gives a similar verification case based on modal logic S4.
【Keywords】theorem proving, model checking, modal logic, S4

１．はじめに可能にしたことや、また、それによる認証に関する安全参考文献４）および５）において、当時開発されてい性証明の形式化は後のプロトコルの安全性検証のためのた食品産業向け商品処理装置のソフトウェア更新システ

論理の研究に大きな影響を与えたが、一方、その無矛盾ムの検証事例が報告されている。そのシステムは工場内性の証明や意味論の確立に課題が知られている（参考文のネットワーク中継装置を介して工場内の商品処理装置献 ８））。LTL モ デ ル 検 査 は 線 形 時 相 論 理（Temporalが工場外のネットワーク上にある管理サーバに接続し、Linear-Time logic）の意味論に基づくモデル検査であり、更新ソフトウェアが管理サーバから商品処理装置へダウ自動車や家電などの組込みコンピュータをはじめとするンロードされるということを実現するものである。また、様々なコンピュータシステムの検証においてその適用がその検証事例における検証手法は形式手法と呼ばれる数その支援ツールである SPIN と共に広がりつつある（参理論理学を基礎とした幾つかの検証手法のうち、BAN

考文献７））。

論理に基づく定理証明と LTL モデル検査が用いられて本稿は参考文献４）および５）が与えた異なる論理をいる。ここで、定理証明とはシステムに与えられた条件・用いた定理証明およびモデル検査による検証に対して、性質から安全性など検証したい性質の数理論理学的な証共通の論理を用いたそれぞれの検証を報告する。先行研

明可能性を検討するという手法である。モデル検査はシ

究では、LTL モデル検査による脆弱性解析と BAN 論

ステムの振る舞いを数理論理学的モデルとして表現し、理による修正の妥当性証明が行われている。そして、そその振る舞いを網羅的に探索することでそのモデルが検れらを整合するために検証対象であるシステムの仕様に証したい性質を満たすか否かを確認するという手法であ立ち戻ってそれぞれの結果を検討している。本稿における。BAN 論理は信念の論理に分類されるものであり、る研究では、様相論理 S4の意味論に基づくモデル検査

プロトコルの安全性検証のために提案された論理推論体

による脆弱性解析と S4の構文論に基づく修正の妥当性

系としては最も早期のものの１つである（参考文献１））。

証明を行い、先行研究と同じ結論を得た。加えて、本研

BAN 論理が安全性などの性質について形式的な分析を究では検証対象まで戻らずに検証対象を抽象化して表現― 95 ―

公立鳥取環境大学紀要

第14号

した状態遷移図および S4におけるモデルと公理系におこのシステムは商品処理装置、中継装置、管理サーバ、いて脆弱性発見および修正を行った。つまり、検証対象コード署名局の４つのエージェントからなる。商品処理そのものまで立ち戻ることなく検証対象からの抽象物に装置は工場内にある中継装置（プロキシ）を経由してイおいて検証対象の脆弱性に関わる本質的な部分のみの考ンターネットに接続し、管理サーバに INF ファイル（こ察によってそれらを行った。また、BAN 論理においてのシステムでは、現在のソフトウェアの版情報などを記証明された性質について、S4という無矛盾性の証明お載したもののこと）や、更新要求を送信する。管理サー

よび意味論が確立された論理体系を用いてその性質を証

バはコード署名局から認証を得た更新 INF ファイルお明することにより、その証明と結果の信頼性を高めた。

よび更新プログラムを商品処理装置から受信した INF

本研究で用いた S4は古典命題論理に次のＫ、Ｔ、４ファイルを基に商品処理装置へ向けて送信する。その際、と呼ばれる公理および必然化の規則と呼ばれる推論規則

それらのファイルはインターネットを介して、中継装置を加えたものである。

を経由して商品処理装置に受信される。ここで、中継装Ｋ：□（Ａ→Ｂ）→（□A →□B）．

置は商品処理装置と管理サーバの間にあって通信の受け

Ｔ：Ａ→Ａ． ４： A →渡しを行うのだが、例えば、商品処理装置から送信され

□A．

□□

た INF ファイルや管理サーバから送信された更新 INF

Ａ□ファイルおよび更新プログラムを記憶して置き、商品処A

理装置に対しては管理サーバの代わりに更新 INF ファ

これらを加えることで、論理式□A は「その時点を含イルと更新プログラムの送信を行い、管理サーバに対しむ以降の時点においてＡ」という解釈ができる。また、ては商品処理装置の代わりに更新 INF ファイルと更新◇A はプログラムの要求を送信し、それらを受信するという役□A の略記として与えることができ、それは「その時点を含む未来のある時点においてＡ」という解割を持つ。

釈ができる。そして、論理式Ａは「１つの時点において図２は商品処理装置、中継装置、管理サーバという３Ａ」という解釈となる。実際、S4のクリプキ意味論はつのエージェントの通信プロトコルの仕様である。商品

半順序関係（反射的かつ推移的関係）を持つ構造に対し処理装置が中継装置に向けて INF ファイルを送信し、て完全である（S4においてＡが証明可能であるとき、中継処理装置がそれを受信した後、管理サーバに送信す

かつそのときのみ任意の半順序構造においてＡが恒真でる。その後、更新プログラムがある場合、中継装置に対ある）ことが示される。本研究において用いる体系につして更新ありとの回答を送信し、中継装置はそれを商品いて、構文論は参考文献３）および６）において与えて処理装置に送信する。そして、中継装置は商品処理装置いるシーケント計算の体系を用いる。また、意味論は参の代わりに更新 INF ファイルおよび更新プログラムの考文献２）および６）において与えられているクリプキ要求を管理サーバに対して送信する。管理サーバは中継意味論を用いる。

装置から要求を受信した後、更新 INF ファイルと更新プログラムを中継装置に送信する。その後、商品処理装２．ソフトウェア更新システム

置から更新 INF ファイルおよび更新プログラムの要求

図１は対象となるソフトウェア更新システムの概念図を中継装置が受信した場合、中継処理装置はそれらを商である。

図１

図２

ソフトウェア更新システム概要― 96 ―

プロトコル仕様吉田

ソフトウェア更新システムプロトコルの様相論理 S4に基づく検証品処理装置に送信する。
図２のプロトコルはインターネット等を介しての通信は行わないコード署名局は省かれている。
図２における通信は実際には共通鍵暗号系による暗号通信が用いられる。また商品処理装置は INF ファイルを送信する際、公開鍵暗号系を用いた署名を行う。管理

図３

サーバも更新 INF ファイルと更新プログラムに対して状態遷移図

署名を行い、これによって、受信したファイルの送信元の確認を可能にしている。

― receive（A, F）：エージェントＡによるＦの受信を

参考文献４）と５）では、このシステムのプロトコルに従って商品処理装置が２つのファイルの更新を要求し表す述語。
―

たとき最新版を得ることができるかということについて

sign（A, F）：ファイルＦがエージェントＡに署名されていることを表す述語。

検証を行っている。その際、そこでは検証対象のプロト

上記の図３の丸で囲まれたＭ、Ｐ、Ｃは状態遷移図にコルをその検証内容に関係する部分を抽出して定理証明おける状態である。ここでは、システムにおける３つのおよびモデル検査を行っている。そこで抽出されたものエージェントを状態としている。状態から他の状態へのは図２における（＊）の箇所である。それらはその検証遷移を表す矢印は対応するエージェントからエージェン

項目に関係する INF ファイルおよび更新ファイルの送トへのファイルの送信に対応する。以下、図３の各遷移信の箇所である。また、先行研究では暗号通信に関してにおけるガード（Ⅰ）から（Ⅸ）の詳細を述べる。

共通鍵暗号による通信は正常に機能していることを前提（Ⅰ）send（C, P, INFi）∧ sign
（C, INFi）（i =1, 2）としており、その性質は検証の対象から除外している。

（Ⅱ）send（C, P, INFi）∧ sign
（C, INFi）

一方、ファイルに付された署名については検証の対象と→ receive（P, INFi）（i =1, 2）している。本研究では、この抽象化された対象の状態遷（Ⅲ）receive（P, INFi）∧ sign
（C, INFi）

移図の作成から行う。

→ receive（M, INFi）（i =1, 2）（Ⅳ）receive（M, INFi）∧ sign
（C, INFi）

３．状態遷移図→ send（M, P, INFi＋1）∧ sign
（M, INFi＋1）（i =1, 2）

状態遷移図とは、状態と呼ばれる点と、それらを結ぶ（Ⅴ）send（M, P, INFi＋1）

有向辺からなる図的表現である。出発点となる状態があ→ send（M, P, Fi＋1）∧ sign
（M, Fi＋1）（i =1, 2）

り、そこから有向辺によって結ばれる状態へと遷移する。 （Ⅵ）send（M, P, INFi＋1）∧ sign（M, INFi＋1）
ただし、有向辺にはガードと呼ばれる含意命題が付随し→ receive（P, INFi＋1）（i = 1, 2）ており、その前条件を満たしたときのみその遷移が可能（Ⅶ）send（M, P, Fi＋1）∧ sign
（M, Fi＋1）となる。前条件を満たし状態が遷移したとき、その遷移先の状態においてその後条件が成り立つ（状態遷移図の→ receive（P, Fi＋1）（i = 1, 2）（Ⅷ）receive（P, INFi＋1）∧ sign
（M, INFi＋1）

詳細については参考文献７）１章１節など）。

→ receive（C, INFi＋1）（i = 1, 2）

前節の抽象化された対象を状態遷移図で表すために図（Ⅸ）received（P, Fi＋1）∧ sign（M, Fi＋1）２における各要素を表す記号や述語を定める。ここで、→ receive（C, Fi＋1）（i = 1, 2）

INF ファイルおよびプログラムの版数は簡単のためそこの状態遷移図が図２のシーケンスチャートの通信内れぞれ３つとする。

容を表現していることは、そのシーケンスチャートの各―

INFi：商品処理装置にインストールされているファ

通信と状態遷移図における各状態遷移が対応しているこ

イルの版情報などを記載したファイル。ここでは３とを示すことで確認できる。ただし、状態遷移図においつ用意されているものとし、i ＝1, 2, 3とする。て、中継装置Ｐの送信に関するガードが含まれていない。

Fi：プログラム。i ＝1, 2, 3。INF1、INF2、INF3 の

これは、中継装置が受け取って渡すという機能だけのもそれぞれに対応したソフトウェア。のであることから、Ｐによる送信は省略してガード（Ⅲ）
、

Ｍ：管理サーバ。Ｐ：中継装置。Ｃ：商品処理装置。

（Ⅶ）、（Ⅷ）はＰがファイルを受信したらそのファイルsend（A, B, F）：エージェントＡからエージェントをそのまま管理サーバＭまたは商品処理装置Ｃが受信すＢへのファイルＦの送信を表す述語。

るということにしている。

―――― 97 ―公立鳥取環境大学紀要

第14号（Ⅰ）について、前提条件無しで send
（C, P, INFi）とである。さらに、◇Ａはsign（C, INFi）が成り立つ場合があることを表している。

□A の略記であることから、ａ｜＝◇Ａ ⇔ ある時点が存在して、aRb かつｂ｜＝Ａ

また、この状態遷移図の各状態には自分自身の状態に戻ってくる矢印が記載されている。これは図２などにはが成り立つ。S4フレームにおいて各原子論理の真偽が定明示されていないことであるが、実際にプロトコルにそ義されたものを S4モデルと呼ぶ。与えられた S4モデルのような冗長性を与え得るという観点と、S4のモデルと論理式に対して、その論理式がそのモデルのすべてのを与えるための便宜を図る観点からそのようにしている。

時点において真であるとき、その論理式はそのモデルにおいて真であるという。また、与えられた S4フレームと４．モデル検査

論理式に対して、任意の原子論理式の真偽の定義の仕方

与えた状態遷移図においてＣは適切な更新プログラム

による S4モデルにおいてその論理式が真である場合、を受信できない振る舞いを探索する。ここで、様々な状

その論理式はその S4フレームにおいて恒真であるという。

態遷移の仕方のうち、悪意のある者にＰが乗っ取られた前述の１～５の振る舞いを S4モデルとして表現する。

場合を考える。例えば、ＰはＣから受信した INF ファ集合について、図３の状態遷移図において前述の１～７イルをそのまま管理サーバＭに送信せず、以前Ｃから受の振る舞いを表す遷移の実行の順番を選ぶ。半順序関係

信した古い INF ファイルをＭに送信するという状況をについて、遷移実行の順番の前後関係を選ぶ。そして、考える。

Ｐが既に INF1 を受信しそれを保持していることを表現

１．既にＰが INF1を持っているとする。

するため、すべての時点において receive（P, INF1）と２．Ｃが INF2をＰに送信する。

sign（C, INF1）が成り立つものとする。以下がその S4モ

３．Ｐは INF2ではなく、INF1をＭに送信する。

デルの詳細である。

４．Ｍは INF1を受信し、INF2および F2をＰに送信す①

る。

send（C, P, INF2）,sign（C, INF2）,receive（P, INF1）,sign（C, INF1）

５．Ｐは既に持っている INF2と F2を受信する。

↓②

６．Ｐは INF2と F2をＣに送信する。
７．Ｃは INF2と F2を受信する。

receive（P, INF2）,sign（C, INF2）,receive（P, INF1）,sign（C, INF1）

このような振る舞いを図３の状態遷移図は許容することを確認することができる。このことの検査を行うため↓③に、その検証項目を表す論理式を与える。

receive（M, INF1）,receive（P, INF2）,sign（C, INF2）,receive（P, INF1）,sign（C, INF1）（send（C, P, INF2）∧ sign（C, INF2）→◇receive（C, INF3））□

この論理式において、Ｃが INF2 に署名しそれを送信す↓④

send（M, P, INF2）,sign（M, INF2）,

れば、INF2 に対して適切な更新 INF ファイルである

receive（P, INF2）,sign（C, INF2）,

INF3を受信するということを表す。

receive（P, INF1）,sign（C, INF1）

ここで、S4のクリプキ意味論を与える。S4フレームとは、空でない半順序集合のことである。空でない集合↓⑤

send（M, P, F2）,sign（M, F2）,Ｓとその上の半順序関係Ｒに対して、本稿では S4フレー

receive（P, INF2）,sign（M, INF2）,sign（C, INF2）,

ムの元を時点または可能世界と呼ぶ。与えられた時点ａreceive（P, INF1）,sign（C, INF1）と論理式Ａに対して、「ａにおいてＡ」であるとき、

↓⑥ａ｜
＝Ａ

receive（P, INF2）,sign（M, INF2）,sign（C, INF2）,receive（P, INF1）,sign（C, INF1）と表記する。次に、すべての原子命題に対して各時点における真偽が定義されたとき、原子命題から作られる各↓⑦

receive（P, F2）,sign（M, F2）,論理式の真偽は論理式の構成に関する帰納法により定義

receive（P, INF2）,sign（M, INF2）,sign（C, INF2）,される。特に、

receive（P, INF1）,sign（C, INF1）↓定義ａ｜＝□Ａ ⇔ 任意の時点ｂに対して、aRb ならばｂ｜＝Ａ⑧― 98 ―

receive（C, INF2）,sign（M, INF2）,

吉田

ソフトウェア更新システムプロトコルの様相論理 S4に基づく検証

receive（P, INF2）, sign（M, INF2）, sign（C, INF2）,〔公理系１〕

receive（P, INF1）, sign（C, INF1）⑴□⑵□（sign（P, X）→ □sign（P, X））↓⑨（X ∈｛INF1, INF2, INF3, N1, N2, N3｝）

receive（C, F2）, sign（M, F2）,（sign（M, X）→ □sign（M, X））

receive（C, INF2）, sign（M, INF2）,receive（P, INF2）, sign（M, INF2）, sign（C, INF2）,⑶

receive（P, INF1）, sign（C, INF1）
子命題が記述されている。署名は一度なされたら常にそれがどの状態においても常に保持されることから、署名⑷のある時点で現れている sign はそれ以降の時点におい⑸ても現れている。③ではＰが INF2ではなく INF1をＭに送信した状況を示す。④ではＭが INF1に対する更新ファイルとして INF2に署名してそれをＰに送信している。

⑹

さて、この S4モデルにおいて、（①｜＝□）⑺

send（C, P, INF2）∧ sign
（C, INF2）→◇receive（C, INF3）は成立しない。実際、⑻（C, INF2）①｜＝send（C, P, INF2）∧ signが成り立つがことは明らかであるが、receive（C, INF3）はどの時点においても偽であることから、⑼①｜＝◇receive（C, INF3）は成り立たない。したがって、検証項目の論理式はこの⑽モデルにおいて偽である。

send（C, P, INFi）∧ sign
（C, INFi）（receive（P, INFi）∧ sign
（C, INFi）□

を表す原子命題 sign はある時点で真である場合、それ以降のすべての時点で真であるため、上記の S4モデル（□

この S4モデルについて、各時点において真である原（X ∈｛INF1, INF2, INF3, F2, F3,｝）→◇receive（P, INFi）（i = 1, 2）→◇receive（M, INFi）（i = 1, 2））））（→◇send（M, P, INFi＋1）∧ sign
（M, INFi＋1）（→◇（send（M, P, Fi＋1）∧ sign
（M, Fi＋1）□□

receive（M, INFi）∧ sign（C, INFi）（i = 1, 2））

send（M, P, INFi＋1）（i = 1, 2））（send（M, P, INFi＋1）∧ sign
（M, INFi＋1）（send（M, P, Fi＋1）∧ sign
（M, Fi＋1）（

receive（P, INFi＋1）∧ sign
（M, INFi＋1）（receive（P, Fi＋1）∧ sign
（M, Fi＋1）

□□

□

□

→◇receive（P, INFi＋1）（i = 1, 2）→◇receive（P, Fi＋1）（i = 1, 2）））→◇receive（C, INFi＋1）（i = 1, 2）→◇receive（C, Fi＋1）（i = 1, 2））

同様に、Ｃが INF2に署名しそれを送信すれば INF2にここで、各公理は □（A →◇B）という形をしている。

対して適切な更新プログラムである F3 を受信するといこれは「ＡをトリガーとしてＢが生じる」ということがうことを表す次の論理式も、この S4モデルによって偽常に成り立つということを表している。公理系１の⑴にになることを示すことができる。

ついて、１度なされた署名はその後常に成り立ち続けることを表している。

（□

公理系１の各論理式が３節で与えた S4モデルにおい）send（C, P, INF2）∧ sign
（C, INF2）→◇receive（C, F3）て成り立つことは容易に確認できる。例えば、公理系１の⑴について、sign（P, INF1）、sign（P, INF2）は①から５．形式化⑤のいずれにおいても成り立っており、それ以外は成り脆弱性の発見としては３節で述べたことで十分である

立っていない。つまり、sign（A, X）が成り立っていなが、さらにここで与えた２つの論理式がこのプロトコルい箇所においては常に□sign（A, X）が成り立っていないにおいて証明できないということまで述べる。そのためので、公理系１の⑴は①から⑤のいずれにおいても成りに、プロトコルを表現する公理系を与え、ここで与えた立つ。公理系１の他の公理も同様にその S4モデルで成モデルがその論理体系における公理を満たすということり立つことが確認できる。

を確認する。
公理系は図３の状態遷移図のガードを基に与える。

S4の健全性（与えられた論理式が S4の形式体系において証明可能ならば任意の S4フレームにおいてその論― 99 ―

公立鳥取環境大学紀要

第14号（（（（（（（（（（理式は恒真）より、与えられた論理式が S4に公理系１を加えた形式体系において証明可能ならば公理系１の各論理式を真とする任意の S4モデルにおいてその論理式⑺□（（１ □２ □））send（C, P, INF2）∧ sign
（C, INF2）→◇receive（C, INF3））∧ send（M, P, Ni）∧ fresh（Ni）（i = 1, 2）

send（M, P, INFi＋1）∧ sign
（M, INFi＋1）

send（C, P, INF2）∧ sign
（C, INF2）→◇receive（C, F3））） ）））））））∧ send（M, P, Ni）∧ fresh（Ni）

send（M, P, Fi＋1）∧ sign
（M, Fi＋1）→◇は真となる。したがって、次の２つの論理式（send（M, P, INFi＋1）⑻□∧ send（M, P, Ni）∧ fresh（Ni）∧ sign
（C, Ni）→◇

は S4に公理系１を加えた形式体系において証明不可能であることが導かれる。

receive（P, INFi＋1）∧ receive（P, Ni）∧ fresh（Ni）（i = 1, 2）

send（M, P, Fi＋1）∧ sign
（M, Fi＋1）

６．常に適切な更新ソフトウェアを得るための修正
古い INF ファイルにすり替えられることを防ぐため⑼□→◇に、商品処理装置は INF ファイルと共に自身がランダムに生成した文字列（これをナンスと呼ぶ）を送信する形に修正することを参考文献４）では提案している。この節では公理系１をナンスの署名と送信を考慮した次の修正版を与える。そのために、新たに記号および述語を定
Ni：ナンス。i ＝1, 2, 3。

―

fresh（Ni）：ナンス Ni は新規に生成されたことを表す述語。i ＝1, 2, 3。

⑽

□→◇

⑾

□（sign（P, X）→ sign（P, X））□□⑶□（X ∈｛INF1, INF2, INF3, F2, F3,｝）⑷

（i=1, 2）

る場合においてファイルの送受信が可能であるものとし（X ∈｛N1, N2, N3｝）した時点で否定される。公理系２の⑶は新規性が否定さ）））（（））

れたら以降は常にそのナンスは新規ではないということを表している。公理系２の⑾はその新規性の終了時点を

receive（P, INFi））（i = 1, 2）∧ receive（P, Ni）∧ fresh（Ni）∧ sign（C, Ni）
receive（M, INFi）∧ receive（M, Ni）∧ fresh（Ni）（i = 1, 2）∧ receive（M, Ni）∧ fresh（Ni）∧ sign（C, Ni）→◇

示している。
ＣからＣの署名付き INF2および署名付きナンス N2を∧ receive（P, Ni）∧ fresh（Ni）

receive（M, INFi）∧ sign（C, INFi）□fresh（Ni）

send（C, P, INFi）∧ sign
（C, INFi）→◇⑹∧ receive（C, Ni）∧ている。そして、その新規性は更新ファイルをＣが受信

receive（P, INFi）∧ sign
（C, INFi）□receive（C, Fi＋1）∧ send（C, P, Ni）∧ fresh（Ni）∧ sign（C, Ni）→◇⑸∧ receive（P, Ni）∧ fresh（Ni）∧ sign（C, Ni）

fresh（X））

fresh（X）→□（（（（（（□fresh（Ni）（i=1, 2）あり、それが新たに生成したものであることが確認でき（sign（M, X）→□sign（M, X））（∧ receive（C, Ni）∧

ここで、ナンスＮは商品処理装置Ｃが生成するもので（X ∈｛INF1, INF2, INF3, N1, N2, N3｝）⑵

receive（C, INFi＋1）

received（P, Fi＋1）∧ sign
（M, Fi＋1）〔公理系２〕⑴（i=1, 2）∧ receive（P, Ni）∧ fresh（Ni）∧ sign
（C, Ni）→◇□receive（P, Fi＋1）∧ receive（P, Ni）∧ fresh（Ni）

received（P, INFi＋1）∧ sign
（M, INFi＋1）

義する。
―∧ send（M, Ni）∧ fresh（Ni）∧ sign（C, Ni）

管理サーバＭに向けて送信すれば、Ｃはいずれ更新ファ
イル INF3および F3を受信するという検証項目を次の論理式で表す。
１２

□

send
（M, P, INFi＋1）∧ sign（M, INFi＋1）∧ send（M, P, Ni）∧ fresh（Ni）（i = 1, 2）□send（C, INF2）∧ sign（C, INF2）））∧ send（C, N2）∧ fresh（N2）∧ sign（C, N2）→◇receive（C, INF3）
send（C, INF2）∧ sign
（C, INF2）∧ send（C, N2）∧ fresh（N2）∧ sign（C, N2）→◇receive（C, F3）

これらの論理式は S4に公理系２を加えた体系において証明可能である（詳細は付記の証明図を参照せよ）。

― 100 ―

吉田

ソフトウェア更新システムプロトコルの様相論理 S4に基づく検証

すなわち、ナンスの導入によって適切な更新がなされることが示される。

tion second edition. CSLI.
３）Troelstra, A., & Schwichtenberg, H.（2000）. Basic
Proof theory, second edtion. Cambrige University

７．まとめと課題

Press.

本稿における研究では、LTL モデル検査による脆弱４）吉田聡・山形頼之（2007）「ソフトウェア更新シス性解析と BAN 論理による修正の妥当性に対する定理証

テムプロトコルの BAN logic による安全性検証」，

明をそれぞれ S4に基づくモデル検査および定理証明

独立行政法人産業技術総合研究所システム検証研究

よって行った。特に、検証対象に立ち戻らずに S4モデ

センター算譜科学研究速報．

ルと公理系に基づいて脆弱性発見と修正を行う事例を与５）山形頼之・斎藤正也（2007）「ソフトウェア更新シえた。

ステムのモデル検査によるセキュリティ」，独立行

ところで、基本的に定理証明とモデル検査を両方実施

政法人産業技術総合研究所システム検証研究センすることが望ましく、さらに理論的にはそれぞれ同一の論理に基づく方がより整合性のある結果と分析が得られ

ター算譜科学研究速報．
６）小野寛晰（1994）「情報科学における論理」，日本評と思われる。その実施手順としては次のようになると考えられる。

論社．
７）中 島震（2008）「SPIN モデル検査―検証モデリン

１．適当な記述言語（仕様記述言語、状態遷移図など）による対象の記述。

グ技法―」，近代科学社．
８）長谷部浩二・BANA Gergei・岡田光弘（2010）「セ２．既存のツールによるモデル検査と定理証明の実施。

キュリティプロトコルの論理的検証法」，萩谷昌巳・

３．S4や古典述語論理など、理論的に既に明らかになっ塚田恭章（著）『数理的技法による情報セキュリている論理によるモデル検査（充足可能性判定も含ティ』，共立出版，pp. 185-202．

む）と定理証明。
（受付日2015年８月28日

しかし、定理証明とモデル検査の両方を実施すること受理日2015年11月11日）

も一般的にはコストが大きく、ましてや同一の論理に基づくものにすることはさらにコストを要する。以上を踏付記：証明図次の論理式が S4および公理系２の下で証明可能であまえると、上記１から着手し、必要に応じて２、３と進めることにならざるを得ない。しかし、１の工程のみ実ることを以降に示す。

施するにしても、２、３への視野を持って行うことが検１

証対象への深い理解につながると思われる。
謝辞（□send（C, INF2）∧ sign（C, INF2））∧ send（C, N2）∧ fresh（N2）∧ sign（C, N2）→◇receive（C, INF3）

なお、次の論理式に対する証明図は以降に示すものと査読者の有用なコメントに感謝を申し上げます。なお、同様であるため、ここでは割愛する。

（

本研究は公立鳥取環境大学特別研究費の助成を受けたも２のです。

□

参考文献

send（C, INF2）∧ sign（C, INF2））∧ send（C, N2）∧ fresh（N2）∧ sign
（C, N2）→◇receive（C, F3）

１）Burrows, M., Abadi, M., & Needham, R.（1990）. A

ところで、以下に与える証明図には明らかと思われる

logic of authentication. DEC SRC Research Report.

推論を省略しており、ギャップが存在する個所を二重線

２）Goldblatt, R.（1992）. Logics of time and computa-

で記している。以下がその省略のある推論である。

― 101 ―

公立鳥取環境大学紀要

第14号

ここで、Γは論理式の集合を表し、∧Γはそこに含る。（box）について、古典命題論理のシーケント計算

まれるすべての論理式を論理積∧によって結合した論理の体系にこの推論規則を加えた体系は古典命題論理のヒ式を表す。⑴は公理系２の⑴から S4のシーケント計算

ルベルト流体系に公理Ｋおよび必然化の規則を加えた体の体系において可能な証明可能な推論である。⑵、⑶、系と同値である。
（cut）は命題論理の推論規則の１つで⑷は S4のシーケント計算において証明可能な推論であある。以下、証明図を与える。

証明図１

証明図２

証明図３

証明図４

証明図５

証明図６― 102 ―吉田

ソフトウェア更新システムプロトコルの様相論理 S4に基づく検証

証明図７

証明図８

証明図９

証明図10

証明図11

証明図12

証明図13― 103 ―