IEICE TRANSACTIONS on Communications
Verification of Content-Centric Networking Using Proof Assistant
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.
- Publication
- IEICE TRANSACTIONS on Communications Vol.E99-B No.11 pp.2297-2304
- Publication Date
- 2016/11/01
- Publicized
- Online ISSN
- 1745-1345
- DOI
- 10.1587/transcom.2016NEP0013
- Type of Manuscript
- Special Section PAPER (Special Section on Deepening and Expanding of Information Network Science)
- Category
Authors
Sosuke MORIGUCHI
Kwansei Gakuin University
Takashi MORISHIMA
Kwansei Gakuin University
Mizuki GOTO
Kwansei Gakuin University
Kazuko TAKAHASHI
Kwansei Gakuin University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Sosuke MORIGUCHI, Takashi MORISHIMA, Mizuki GOTO, Kazuko TAKAHASHI, "Verification of Content-Centric Networking Using Proof Assistant" in IEICE TRANSACTIONS on Communications,
vol. E99-B, no. 11, pp. 2297-2304, November 2016, doi: 10.1587/transcom.2016NEP0013.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/communications/10.1587/transcom.2016NEP0013/_p
Copy
@ARTICLE{e99-b_11_2297,
author={Sosuke MORIGUCHI, Takashi MORISHIMA, Mizuki GOTO, Kazuko TAKAHASHI, },
journal={IEICE TRANSACTIONS on Communications},
title={Verification of Content-Centric Networking Using Proof Assistant},
year={2016},
volume={E99-B},
number={11},
pages={2297-2304},
abstract={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.},
keywords={},
doi={10.1587/transcom.2016NEP0013},
ISSN={1745-1345},
month={November},}
Copy
TY - JOUR
TI - Verification of Content-Centric Networking Using Proof Assistant
T2 - IEICE TRANSACTIONS on Communications
SP - 2297
EP - 2304
AU - Sosuke MORIGUCHI
AU - Takashi MORISHIMA
AU - Mizuki GOTO
AU - Kazuko TAKAHASHI
PY - 2016
DO - 10.1587/transcom.2016NEP0013
JO - IEICE TRANSACTIONS on Communications
SN - 1745-1345
VL - E99-B
IS - 11
JA - IEICE TRANSACTIONS on Communications
Y1 - November 2016
AB - 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.
ER -
English
