Formal Modeling And Verification Of Named Data Networking

Nowadays,the core of the Internet is the TCP/IP protocol,which is designed for end-to-end communication between hosts.With the rapid development of the Internet,both the number of users and the network data contents have increased explosively.Its own defects lead to problems such as low flexibility,congestion and low scalability.To address those issues,there are two international dominant solutions: One is to constantly improve the existing IPv4 protocol to make it transition to the IPv6 protocol.The other is to adopt a new Internet architecture called Information Centric Networking(ICN),which can solve problems at their source.The most representative member of ICN is Name Data Networking(NDN).After the several years' efforts of network researchers around the world,NDN stands out from many ICN research projects and becomes one of the most promising solutions in the future.In NDN,users fous on the content itself rather than its location,which means NDN is driven by data consumption.NDN provides security mechanisms based on the data itself and fairly flexible routing strategies,while improving utilization ratio of resources.This thesis uses formal methods to model and verify NDN.We mainly focus on the application of NDN in wireless network,content access control and routing protocols.Firstly,the application of NDN in wireless network is studied and a security calculus for wireless networks of NDN(SCWN)is proposed to describe the special mechanism of NDN.Then,we use logical analysis and model checking to analyze and model the content access control solution of NDN resepectively,to check whether it can guarantee the security of critical keys and data.Finally,timed automata is applied to model,analyze and verify the NLSR routing protocol.The main contributions of this thesis are as follows:· We propose a security calculus for wireless networks of NDN(SCWN).It introduces a special forwarding and data caching mechanism in NDN,and also adds a new security mechanism of channels to support network security.SCWN calculus specifies a network through both the process level and network level.It adds some special parameters to describe the different processes of Interest packet and Data packet of the wireless node,and the isolated communication betweenthe normal channel and the protected channel.We apply SCWN calculus to the LFBL protocol and portray it successfully.Meanwhile,the graph theory is used to provide a verification scheme for the properties.· We investigate the content access control solution for NDN.Two methods are used to analyze and verify the solution.The first one is logical analysis.By extending the BAN logic,we obtain the improved BAN logic.It is applied to the content access control solution for NDN.We first use logical formulas to describe the premise of the solution.Then,we also depict the process steps of the solution by logical formulas.At last,the security goals are also transformed to logical formulas.We use the improved BAN inference rules to determine whether the security goals can be derived from the process steps.We find out that some security goals could not be derived,which means there are security flaws.Then,practical assumptions are added to support the derivation of security goals.As a result,the security of the content access control solution is improved.· We continue to focus on the content access control solution for NDN by using model checking.We use CSP to model the behavior of readers,writers and an access control manager.In order to simulate the real situation,intruders,invaded readers,and invaded writers are added to the model.Some safety-related properties are described in linear temporal logic(LTL)and then verified by model checker PAT.In the verification process,we find invalid properties and then do practical model improvements,which supports the valid verification results of the properties.· We use timed automata to model NLSR routing protocol for NDN.We verify the synchronization of LSDB maintained by each routing node.Model checker UPPAAL supporting timed automata is applied to implement the forwarding mechanism of NDN and synchronization mechanism of the NLSR protocol.It verifies the related properties of the model.Then we test several network topology scenarios and find two special scenarios that can not accomplish synchronization.The corresponding solutions are proposed to improve the robustness of the protocol.