命名数据网络的形式化建模与验证

发布时间：2020-05-10 08:55

【摘要】：目前,互联网的核心是TCP/IP协议,该技术的设计初衷是针对端到端的主机通信。但随着互联网的高速发展,互联网用户的数量爆炸式增长的同时,网络数据内容也在急剧膨胀,它的自身缺陷会导致灵活性低、易拥塞、扩展性低等问题,以至于无法应对日益增长的大规模数据内容分发。为了解决这些问题,国际上有两种主流的方法:一种是不断改进现有的IPv4协议使其过渡到IPv6协议;另一种是从根本上去解决问题,即采用全新的互联网体系架构信息中心网络(Information Centric Networking,ICN)。ICN中最具代表性的就是命名数据网络(Name Data Networking,NDN),经过多年研究,它在全球各地网络研究者的努力下逐步发展,从众多ICN研究项目中脱颖而出,被认为是当前最有发展前景的方案之一。在命名数据网络中,用户关注的重点不在于内容的位置,而在于内容本身,即以数据消费为驱动。命名数据网络提供了基于数据本身的安全机制和相当灵活的路由策略,同时提高资源重复利用率。本文采用形式化方法开展了对命名数据网络的建模与验证,我们主要着重于命名数据网络在无线网络上的应用、内容访问控制和路由协议三个方面进行深入研究。首先,研究了命名数据网络在无线网络中的应用,提出了命名数据网络的安全无线网络演算(SCWN),在演算中刻画它的特殊机制。然后,分别使用逻辑化分析和模型检测的方法对命名数据网络内容访问控制解决方案进行分析和建模,检验它是否能保证关键密钥和数据的安全性。最后,应用时间自动机对NLSR路由协议进行建模、分析和验证。本文的主要内容与贡献包括:·本文提出了命名数据网络的安全无线网络演算(SCWN)。它引入了命名数据网络中特殊转发机制和数据缓存机制,同时也加入了新的通道安全机制来支持网络的安全性。SCWN演算从进程层面和网络层面对无线网络进行刻画,并加入一些特殊参数,进一步描述了无线节点对Interest包和Data包的不同处理,以及普通通道和受保护通道的隔离通信。本文把SCWN演算应用到了LFBL协议中,成功刻画了该协议,并用图论的方法提供了对性质的验证方案。·本文研究了关于命名数据网络的内容访问控制解决方案。采用了两种方法来对该解决方案进行分析和验证。第一种是逻辑化分析方法,通过对BAN逻辑进行拓展,得到改进的BAN逻辑,并将此应用于命名数据网络的内容访问控制解决方案。本文首先用逻辑公式描述该解决方案的前提,然后把该解决方案的过程步骤也用逻辑公式刻画,最后把该解决方案的安全目标也转化为逻辑公式。之后采用改进的BAN逻辑的推理规则,来判断是否能从该解决方案的过程步骤推导出其安全目标。发现存在一些安全目标无法被推导,即存在安全漏洞。于是增加了符合实际的新假设来支持安全目标的推导,从而提高了内容访问控制解决方案的安全性。·本文继续针对命名数据网络的内容访问控制解决方案,采用了第二个形式化方法——模型检测。使用通信顺序进程(CSP),对该解决方案中的读取者、写入者和访问控制管理器这些实体的行为进行建模。为了模拟真实情况,在模型中加入入侵者、被入侵的读取者和被入侵的写入者。使用线性时态逻辑(LTL)对一些安全相关的性质进行描述,而后借助模型检测工具PAT对其进行验证。在这过程中,我们发现了一些无法验证通过的性质,进而对模型进行符合实际的改进,支持了性质的验证。·本文使用时间自动机对命名数据网络的NLSR路由协议进行建模。针对每个路由节点上维护的LSDB是否同步进行验证。采用支持时间自动机的模型验证工具UPPAAL对命名数据网络的转发机制和NLSR协议的同步机制进行了实现,并验证了模型相关性质。之后测试了多个网络拓扑场景,找出了两个无法完成同步的特殊场景,给出对应的解决方案,进而提高了协议的鲁棒性。
【图文】：

本性,验证结果,模型基,节点

图 6.5 NLSR 模型基本性质的验证结果A B0 0A B0 0Produce N1Interest Name Interfaces/sync-prefix/1000 0PIT of Router A and B:Interest Name InterfacesPIT of Router A and B:①②(a) 节点A和B相互发送SyncInterest包。(b) 节点A产生了名字 N1并更新了自己的名字集合。然后根据他们在(a)中各自的PIT，，按顺序完成 SyncData包的返回。A B0 0Interest Name Interfaces/sync-prefix/1111 0PIT of Router A :(c) 节点B产生名字N2和N3。节点A和B相互发送Sync Interest包。Produce N2and N3Interest Name Interfaces/sync-prefix/1100 0PIT of Router B:Digest=1000 Digest=1000Digest=1100 Digest=1100Digest=1100 Digest=1111图 6.6 NLSR 模型第一个测试场景中路由器 A 和 B 之间的通信关系。表 6.2 NLSR 模型测试场景中出现的名字集合和摘要的关系
【学位授予单位】：华东师范大学
【学位级别】：博士
【学位授予年份】：2018
【分类号】：TP393.0

【相似文献】