For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Verification of Content-Centric Networking Using Proof Assistant
Sosuke MORIGUCHI Takashi MORISHIMA Mizuki GOTO Kazuko TAKAHASHI
IEICE TRANSACTIONS on Communications
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)
Content-Centric Networking, proof assistant, network topology, protocol verification,
Full Text: PDF(1.1MB)>>
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.