Formalization of the Behavior of Content-Centric Networking

Content-Centric Networking (CCN) is a communications architecture that is based on the names of contents, rather than on ad- dresses. The protocol used in CCN does not apply to end-to-end communications but is, instead, for network-wide communications. Each node sends packets to the nodes that are connected to it, which communicate with further nodes that are connected to them. When data are sent, the receiving nodes store the data and forward it to other nodes. Such data storage increases reliability and divides the load among servers; however, the behavior and performance of the protocol requires further investigation. In this paper, we formalize the CCN protocol using the proof assistant Coq. There are two aspects of this formalization: the network module type and the behavior of the protocol. The network module type has several parameters, including the data type denoting nodes, connection relations between nodes, and some status depending on the CCN. We then give proofs of two specifications for content- delivery in CCN. With a specific network description based on the module type, we obtain proofs of these specifications of the given network directly. This result can be used to enhance the reliability of CCN protocols.