Modeling and verifying NDN access control using CSP

Named Data Networking (NDN) is a new promising architecture of information-centric networking. NDN could not reuse the existing access control solutions designed for the IP architecture due to their fundamental difference of design, as well as NDNs caching property. As a result, several access control solutions have been proposed for NDN. One of them is specially for both closed and open environment. In this paper, we make the very first attempt to model and verify several important properties of NDN access control. We adopt CSP (Communicating Sequential Processes) to model the NDN access control proposed by Hamdane et al., as well as their security properties. By feeding the models into the model checker PAT (Process Analysis Toolkit), we have verified that the NDN access control cannot prevent the NK key pair faking and the data leakage with the appearance of intruders. We introduce a new method to solve these issues. Considering the situation when the entities are invaded, we also improve our method to make the NDN access control strong enough to maintain the property of key authenticity and data security in this vulnerable situation. We hope that our study would help enhancing the adaptability and robustness of the NDN access control.