Verification of Content-Centric Networking Using Proof Assistant

Sosuke MORIGUCHI  Takashi MORISHIMA  Mizuki GOTO  Kazuko TAKAHASHI  

Publication
IEICE TRANSACTIONS on Communications   Vol.E99-B   No.11   pp.2297-2304
Publication Date: 2016/11/01
Online ISSN: 1745-1345
Type of Manuscript: Special Section PAPER (Special Section on Deepening and Expanding of Information Network Science)
Category: 
Keyword: 
Content-Centric Networking,  proof assistant,  network topology,  protocol verification,  

Full Text: PDF(1.1MB)
>>Buy this Article


Summary: 
In this paper, we give a formalization of the behavior of the Content-Centric Networking (CCN) protocol with parameterizing content managements. CCN is a communications architecture that is based on the names of contents, rather than on addresses. In the protocol used in CCN, each node sends packets to the nodes that are connected to it, which communicate with further nodes that are connected to them. This kind of behaviors prevents formalizing the CCN protocol as end-to-end communications. In our previous work, we formalized the CCN protocol using the proof assistant Coq. However, in this model, each node in the network can store any number of contents. The storage for each node is usually limited and the node may drop some of the contents due to its filled storage. The model proposed in this paper permits a node to have its own content management method, and still keeps the temporal properties that are also valid in the previous model. To demonstrate difference between these models, we give a specification that is valid in the previous model but invalid in the proposed model, called orthogonality. Since it is generally invalid in CCN, the proposed model is more precise than the previous one.