Verification of Content-Centric Networking Using Proof Assistant

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.