通信プロトコルにおけるサービス不能攻撃耐性のための型付π計算

冨岡 大悟; 池田立野; 西崎真也

doi:10.11309/jssst.23.3_66

論文・著書情報

タイトル

和文:	通信プロトコルにおけるサービス不能攻撃耐性のための型付π計算
英文:

著者

和文:	冨岡大悟, 池田立野, 西崎真也.
英文:	冨岡大悟, Ritsuya Ikeda, Shin-ya Nishizaki.

言語

Japanese

掲載誌/書名

和文:	コンピュータソフトウェア
英文:

巻, 号, ページ

Vol. 23 No. 3 pp. 66-84

出版年月

2006年7月

出版者

和文:	日本ソフトウェア科学会
英文:	Japan Society for Software Science and Technology

会議名称

和文:
英文:

開催地

和文:
英文:

DOI

https://doi.org/10.11309/jssst.23.3_66

アブストラクト

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

Home

各種検索

サポート

T2R2について

関連リンク

論文・著書情報