接続表とアドレス変換表の一貫性証明 (2)

pfm_incSecの適用前後で不変表明con_nat_Inv2が成立することを証明する．

命題の設定

pfm_incSecは，pfm_incSec1をn回繰り返すメソッドであるため，実際には，pfm_incSec1 の適用前後で不変表明が成立することを証明すれば，pfm_incSecの適用前後でも成立す ることがいえる．

証明対象の命題は次のようになる．

let s1 = pfm_incSec1 pfm s in

Pre2 pfm s /\ con_nat_Inv2 pfm s ==> con_nat_Inv2 pfm s1

つまり，ストアsについてcon_nat_Inv2が成立することを仮定し，pfm_incSec1の適用 後のストアs1についてcon_nat_Inv2が依然として成立していることを証明する．

証明

9.3^{と同様，次の}2^{つの補題を証明する．}

(A) !pfm s. Pre2 pfm s /\ con_nat_timer_Inv pfm s ==>

con_nat_timer_Inv pfm (pfm_incSec1 pfm s) (B) !pfm s. Pre2 pfm s ==>

connection_timer_Inv pfm (pfm_incSec1 pfm s) 以下，補題(A)(B)を順に証明する．

補題(A)の証明

証明対象の命題は次の通りである．

!pfm s. Pre2 pfm s /\ con_nat_timer_Inv pfm s ==>

con_nat_timer_Inv pfm (pfm_incSec1 pfm s)

まず，全称量子を除去し ，con_nat_timer_Invの定義を展開する．

Pre2 pfm s /\

(!lap gap t.

pfm_connectionExistsWithTime pfm lap gap t s ==>

pfm_srcnatRuleExistsWithTime pfm lap t s) ==>

(pfm_connectionExistsWithTime pfm lap gap t (pfm_incSec1 pfm s) ==>

pfm_srcnatRuleExistsWithTime pfm lap t (pfm_incSec1 pfm s)) ここで，次の定理が成立することに着目する．

|- !pfm s. Pre2 pfm s ==>

(pfm_connectionExistsWithTime pfm lap gap t (pfm_incSec1 pfm s) = pfm_connectionExistsWithTime pfm lap gap (SUC t))

つまり，すべての接続についてタイムアウト時間を 1減算した直後に，lapとgapの間の 残り時間がtとなっている接続が存在することは，タイムアウト減算前にlapとgapの間 の残り時間がSUC tとなっている接続が存在することと同値である（ 図9.9上段）．この 定理は，定義を展開後，接続表を表す次の項

contable_get_connectionList (pfm_get_contable pfm s) s に関する帰納法を用いて証明することができる（ 証明略）．

アドレス変換表についても同様に次の定理が成立する．

|- !pfm s. Pre2 pfm s ==>

(pfm_srcnatRuleExistsWithTime pfm lap t (pfm_incSec1 pfm s) = pfm_srcnatRuleExistsWithTime pfm lap (SUC t))

つまり，すべてのアドレス変換規則についてタイムアウト時間を 1減算した直後に，lap に対応する残り時間がtとなっている変換規則が存在することは，タイムアウト減算前に lapに対応する残り時間がSUC tとなっている変換規則が存在することと同値である（図 9.9下段）．

nattable contable

(lap,gap,t)

(lap,_,t) contable

nattable pfm_incSec1 pfm s

(lap,gap,t+1)

(lap,_,t+1)

pfm_incSec1 pfm s ...

...

...

...

...

...

...

...

...

...

図9.9: pfm incSec1による接続表とアドレス変換表の変化

これらの定理を用いてゴ ールを簡単化すると，次のようになる．

Pre2 pfm s /\

(!lap gap t.

pfm_connectionExistsWithTime pfm lap gap t s ==>

pfm_srcnatRuleExistsWithTime pfm lap t s) ==>

(pfm_connectionExistsWithTime pfm lap gap (SUC t) s ==>

pfm_srcnatRuleExistsWithTime pfm lap (SUC t) s)

後は，前提条件の全称量子をそれぞれlap,gap,SUC tに特化すれば証明が完了する．

補題(B)の証明

証明対象の命題は次の通りである．

|- !pfm s. Pre2 pfm s ==>

  connection_timer_Inv pfm (pfm_incSec1 pfm s)

不変表明connection_timer_Invは，pfm_incSec1適用後，適用前の不変表明の仮定 なしで成立する．これが成立する理由は，pfm_incSec1により，すべての接続のタイムア ウト残り時間は 1 減算されるが，減算した結果が 0となる接続は同時に除去されてしま

うからである．したがって，pfm_incSec1の適用後は，残り時間が 0 ^{より大きい接続し} か残っておらず，不変表明が無条件に成立する（詳細略）．

III

付録集

付 録 A パケット フィルタリングシステムの HOL ^コード

パケットフィルタリングシステムのクラスモデル，HOLにおけるメソッド 定義を以下に 示す．