概要

Content-Centric Networking (CCN) とは 2009 年に Van Jacobsen が
提案した通信方式であり,アドレスを利用するのではなくコンテンツ名に注目し
て通信をおこなうものである.CCN では中継ノードでコンテンツをキャッシュす
ることができ,ネットワークの利用効率の向上や,応答時間の短縮が特徴として
挙げられる.現在はシミュレーションをベースとして動作や性能のチェックがお
こなわれているが,CCN は確立した技術ではないため,実用化にむけて動作の正
当性の検証が望まれる.本研究では,証明支援系 Coq を用いて, CCN のプロトコ
ルを帰納的にモデル化し,半直線のライン型ネットワークトポロジと,完全二分
木のツリー型ネットワークトポロジにおいて動作の正当性の検証をした.このモ
デルでは,各ノードでおこなわれているマッチング処理を実装し,1 つの時系列
リストを用意して,ノード間のパケットの送受信すべてを管理するようにした.動
作の正当性として,あるコンテンツがネットワーク上に存在し,ユーザがそれを
要求すれば,必ず正しいものを受信できるかということと,その逆の,コンテンツ
を受信した場合は,そのユーザが要求を送っていたということを証明した.

発表論文
 
"証明支援系Coqを使ったCCNのモデル化と検証について," 
電子情報通信学会ディペンダブルコンピューティング研究会, 
信学技報 Vol.114, No.21, pp.37-42, April, 2014. 

"Coqを使ったツリー型ネットワークトポロジー上でのCCNのモデル化と検証について,"
情報処理学会第103回PRO研究会資料, March, 2015.

"Formalization of the Behavior of Content-Centric Networking," 
The 10th International Conference on Future Networks and Communications (FNC2015), 
Procedia Computer Science, Vol.56, pp.197-204, August, 2015.