通信プロトコルの安全性，特に認証プロトコルにおける認証の正当性に関する研究は，AbadiやGordonによるspi計算(secure pi-calculus)などをはじめとして，近年さかんに行なわれている．プロトコルにおける安全性は，認証の正当性や機密性などの他に，最近では，サービス不能攻撃(Denial-of-Service attack)耐性が重要視される．もっとも典型的な攻撃例としては，TCPの3ウェイハンドシェイクにおけるSYNあふれ攻撃(SYN-flooding attack)が知られている．プロトコルのサービス不能攻撃耐性を形式的に扱う枠組みとしては，メドーズらにより提唱された，コスト情報を付記したアリス・ボブ記法があった．この他に，最近，冨岡らにより提唱されたspice計算[13]がある．spice計算は，spi計算を拡張したもので，プロセスの計算における計算コストが，サーバーやクライアントの計算機において，どのように費されるかを明示的に表現できるように，システムにおける計算機構成を型として形式化した．そして，書き換えスタイルの操作的意味論があたえられており，プロセスに対する型付けの情報を利用することにより，計算の進行における計算コストを区別するようになっている．記憶コストは，サービス不能攻撃耐性を測る場合，各種の計算コストのうちで最も重要となるのだが，spice計算では，記憶領域の解放を明示的に行なうようにした．本研究では，従来のspice計算における型体系と操作的意味論を，計算機ごとの記憶コストの見積りに併せて，記憶領域の解放に関する正当性を保証するように，改良した．また，SYNあふれ攻撃とその防御策であるSYNクッキーが形式化できることを適用例として紹介する．