CN112636919B

CN112636919B - BAN—n逻辑的NLSR安全模型安全分析和验证方法

Info

Publication number: CN112636919B
Application number: CN202011442806.8A
Authority: CN
Inventors: 费媛
Original assignee: Shanghai Industrial Control Safety Innovation Technology Co ltd; Shanghai Normal University
Current assignee: Shanghai Industrial Control Safety Innovation Technology Co ltd; Shanghai Normal University
Priority date: 2020-12-08
Filing date: 2020-12-08
Publication date: 2022-10-18
Anticipated expiration: 2040-12-08
Also published as: CN112636919A

Abstract

本发明BAN‑n逻辑的NLSR安全模型安全分析和验证方法，涉及命名数据网络的域内路由协议安全技术领域。本发明包括：步骤A分析NLSR安全模型，提出BAN‑n逻辑；步骤B抽取NLSR安全模型涉及的节点间LSA数据包的收发过程，应用BAN‑n逻辑进行刻画建模；步骤C利用BAN‑n逻辑的推理规则对数据安全目标和密钥安全目标进行验证；步骤D抽取带入侵者NLSR安全模型涉及的节点间LSA数据包的收发过程，应用BAN‑n逻辑进行刻画建模；步骤E利用BAN‑n逻辑的推理规则对伪造数据入侵目标和伪造密钥入侵目标进行验证。通过BAN‑n逻辑在NLSR安全模型可被验证入侵者无法用伪造密钥和伪造数据实现入侵。

Description

BAN—n逻辑的NLSR安全模型安全分析和验证方法

技术领域

本发明涉及命名数据网络域内路由协议安全模型技术领域，具体指一种BAN-n逻辑的NLSR安全模型安全分析和验证方法。

技术背景

随着互联网用户的不断增长，用户越来越多的关注于信息内容，而拥有端到端的通信机制的IP网络结构对此支持薄弱。因此，信息中心网络(Information CentricNetworking， ICN)得以被提出，它的重点在于信息内容的传播和分发。命名数据网络(Named Data Networking，NDN)是一个源自于ICN架构的针对未来互联网变革性的网络框架。命名数据网络通过使用名字来标记数据包，从而避免携带IP地址。请求方需要数据则发送对应兴趣包(Interest Packet)，在达到有数据的节点会返回数据包(Data Packet)。兴趣包会依照自身所带的内容进行路由，而数据包会沿着兴趣包发送过来的路径返回。

NLSR(Named-data Link State Routing Protocol)是一个命名数据网络的域内路由协议。NLSR使用分发链路状态通告(Link State Advertisement，LSA)来完成网络拓扑结构的构建。每个路由器拥有一个链路状态数据库(Link State Data Base，LSDB)用于存储LSA。如果路由器检测到周围的网络拓扑结构变动或者本地的名字前缀被修改，都会生成一个新的LSA同时传播给整个网络。

每个NDN数据包包括内容名(Content Name)、签名(Signature)和数据(Data) 等。它是经过数字签名认证的，并且在签名信息里有密钥定位器(Key Locator)可以指出签名密钥的名字。为了保证一个拥有有效签名的LSA的合法性，NLSR协议基于信任锚(TrustAnchor)构建了五层安全模型(如附图1所示)。在顶层，有一个根节点(Root)，即信任锚(Trust Anchor)，它用于向站点(Site)发送证书；每个站点有一个或更多操作器(Operator)，而每个操作器管理同属于一个站点的路由器(Router)。每个路由器可以产生一个NLSR路由进程来产生LSA。这种等级信任模型能够建立一串验证LSA密钥。LSA 必须被有效NLSR进程签名。而有效的NLSR密钥必须由对应的路由器密钥签名。同时路由器密钥必须被它所属的站点的操作器密钥签名。每个站点的操作器密钥必须被站点密钥签名，而站点密钥必须被根节点密钥签名。最后根节点密钥完成自我签名。

安全模型属于安全协议范畴为安全提供保障。如果设计出现错误，就无法提供较好的安全服务，其安全性的分析验证显得尤为重要。因此，使用形式化方法对安全模型进行建模和分析是极其合适的。1987年，Needham和Schroeder最早提出了对安全协议的形式化分析。之后，大多数的形式化工具都基于状态检测技术。随着1989年BAN逻辑的提出，安全协议的形式化分析有了一种截然不同的方法。这是一种模态逻辑系统，它是由命题和推理规则组成，是基于知识和信念的推理。

常见的BAN逻辑的推理规则如下表所示

如上所述，BAN逻辑的推理规则简单明了，使用方便，已经被一些著名的安全协议分析应用。

发明内容

本发明的目的在于克服现有技术存在的缺失和不足，提出BAN- n逻辑的NLSR安全模的安全性分析和验证的方法。

本发明思路是，对NLSR安全模型进行了分析，由于安全模型涉及到密钥验证，需要引入密钥验证的相关逻辑符号构件，同时为了描述Data包中内容(Content)部分和签名(Signature)部分，同时引入了相关逻辑符号构件。在此基础上，设定了消息意义规则、管辖权验证规则、密钥验证规则和接收消息规则，即以NLSR安全模型和形式化为基础，提出BAN-n逻辑，同时将其应用于NLSR安全模型，针对其数据安全目标和密钥安全目标进行验证。并且将BAN- n逻辑应用于引入入侵者的NLSR安全模型，针对伪造数据入侵目标和伪造密钥入侵目标来进行验证。

本发明的技术方案：提出BAN- n逻辑并应用于NLSR安全模型，对其进行安全性分析和验证，包括如下步骤：

1.对NLSR安全模型进行分析，提出BAN- n逻辑。

2.提取NLSR安全模型涉及到节点间LSA数据包的收发过程，使用BAN- n逻辑进行刻画。

3.利用BAN- n逻辑中的推理规则，对数据安全目标和密钥安全目标进行验证。

4.提取带入侵者的NLSR安全模型涉及到节点间LSA数据包的收发过程，使用BAN-n逻辑进行刻画。

5.利用BAN- n逻辑中的推理规则，对伪造数据入侵目标和伪造密钥入侵目标进行验证。

如上所述，通过BAN- n逻辑，在NLSR安全模型中应用对其进行安全性分析和验证，可以被验证入侵者无法用伪造密钥和伪造数据来实现入侵。

附图说明

图1为现有NLSR协议基于信任锚(Trust Anchor)构建的五层安全模型；

图2为本发明BAN- n逻辑的NLSR安全模型安全分析和验证方法流程框图；

图3为本发明实施例在NLSR安全模型下节点之间的LSA数据包收发过程图；

图4为本发明实施例在带入侵者的NLSR安全模型下节点之间的LSA数据包收发过程图。

具体实施方式

以下结合附图和实施例对本发明作进一步描述。

实施例，分析的对象为L.Wang等人在IEEE Access杂志上发表的《A Secure LinkState Routing Protocol for NDN》，他们提出了一种命名数据网络NDN的安全链接状态路由协议NLSR，并为该协议的安全性构建出五层的分层信任模型(如附图1所示)。

本发明方法的具体步骤(如附图2所示)：

步骤A.通过对NLSR安全模型进行分析，改进为：BAN- n逻辑，包括BAN- n逻辑符号构建和其语义描述，BAN- n逻辑的推理规则。

所述BAN- n逻辑符号包括如下四个逻辑符号：

P|≈K表示主体P对密钥K进行了密钥验证；

表示由私钥K^-1加密的公式X形成的消息为Data包中Content部分；

({X}_K)_s表示由密钥K加密的公式X形成的消息为Data包中Signature部分；

(K)_c表示由密钥K组成的消息为Data包中Content部分；

所述BAN- n逻辑的推理规则有四种：

包括消息意义规则、管辖权验证规则、密钥验证规则和接收消息规则；

消息意义规则(MM1)

表示如果P相信K为Q的公钥，P收到消息

并且P对密钥K进行了密钥验证，则P相信Q曾经发送过消息X；

管辖权验证规则(JV)

表示如果P和Q对密钥K进行了密钥验证，并且P 收到密钥K，则P相信Q对X拥有管辖权；

密钥验证规则(KV1)

表示对于密钥k属于VK集合，如果P收到{k}_K，P相信K为Q的公钥，并且P收到(k)_c，则P对密钥k进行了密钥验证；

密钥验证规则(KV2)

表示对于密钥k属于DK集合，如果P对所有VK集合中的密钥进行密钥验证，同时VK集合中存在某个密钥k₂使得P满足收到

并且P相信k为Q的公钥，则P对密钥k进行了密钥验证；

接收消息规则(SEE3)

表示如果P收到消息

则P收到消息

接收消息规则(SEE4)

表示如果P收到消息({X}_K)_s，则P收到消息

接收消息规则(SEE5)

表示如果P收到消息(K)_c，则P收到消息X。

步骤B.抽取NLSR安全模型中的节点间LSA数据包的收发过程，给出NLSR安全模型涉及到的相关符号，定义使用到的公式和密钥；保留收发消息中内容部分和签名部分，并给出NLSR安全模型的数据密钥集合DK和验证密钥集合VK，使用BAN- n逻辑对NLSR安全模型进行建模。

步骤C.提取出需要验证的两种安全目标，一个是数据安全目标即保证读者收到了数据、读者相信邻居节点相信数据为真，同时读者相信数据为真，另一个是密钥安全目标即保证读者收到了所有密钥，读者相信邻居相信所有密钥为真，同时读者相信所有密钥为真。使用BAN- n逻辑这两种安全目标进行理想化表达，并使用BAN- n逻辑的推理规则对这两种安全目标进行验证。

步骤D.抽取带入侵者的NLSR安全模型中的节点间LSA数据包的收发过程，使用改进的BAN- n逻辑对其进行建模。

步骤E.提取出需要验证的两种入侵目标，一个是伪造数据入侵目标即保证读者收到了伪造数据、读者相信邻居节点相信伪造数据为真，同时读者相信伪造数据为真，另一个是伪造密钥入侵目标即保证读者收到了伪造的NLSR密钥，读者相信邻居相信伪造的NLSR密钥为真，同时读者相信伪造的NLSR密钥为真。使用BAN- n逻辑这两种入侵目标进行理想化表达，并使用BAN- n逻辑的推理规则对这两种入侵目标进行验证。

(1)改进BAN逻辑得到BAN- n逻辑

实施例，对BAN逻辑进行改进，在表1中给出了BAN逻辑的符号构件及其语义描述。

表1 BAN逻辑的符号构件及其语义描述

对NLSR安全模型进行了分析，由于安全模型涉及到密钥验证，需要引入密钥验证的相关逻辑符号构件，同时为了描述Data包中Content部分和Signature部分，也引入了相关逻辑符号构件。在此基础上，设定了消息意义规则、管辖权验证规则、密钥验证规则和接收消息规则。通过对NLSR进行分析，BAN- n逻辑，如表2。

表2 BAN- n逻辑符号构件及其语义描述

常见的BAN逻辑，如表3。

表3常见的BAN逻辑的推理规则

通过对NLSR进行分析，BAN- n逻辑的推理规则，如表4。

表4 BAN- n逻辑的推理规则

(2)使用BAN- n逻辑对NLSR安全模型进行建模

通过对NLSR安全模型的分析，抽取出了当前路由节点Router和邻居路由节点Neighbor的LSA数据包收发过程(如附图3所示)。

同时，将给出用到安全模型相关的符号及其符号描述，如表5所示。

表5 NLSR安全模型涉及的符号

附图3中节点之间的LSA数据包收发过程，可以写为如下12条消息：

消息1.Router-＞Neighbor：name_Data

消息2.Neighbor-＞Router：

消息3.Router-＞Neighbor：

消息4.Neighbor-＞Router：

key_NLSR

消息5.Router-＞Neighbor：

消息6.Neighbor-＞Router：

key_router

消息7.Router-＞Neighbor：

消息8.Neighbor-＞Router：

key_operator

消息9.Router-＞Neighbor：

消息10.Neighbor-＞Router：

key_site

消息11.Router-＞Neighbor：

消息12.Neighbor-＞Router：

key_root

首先，Router向邻居节点Neighbor发送LSA的Interest包包括了对应LSA的Data包的名字(消息1)；

然后，邻居节点Neighbor向节点Router发送LSA数据包，包括数据名部分、数据部分和签名部分。

数据名部分包括name_Data，内容部分包括由key_NLSR的私钥数据加密得到的

签名部分包括

(消息2)。

其次，节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_NLSR(消息3)。然后，邻居节点Neighbor向节点Router回复有对应名字的带有数据key_NLSR的数据包(消息4)。节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_router(消息5)。

之后，邻居节点Neighbor向节点Router回复有对应名字的带有数据key_router的数据包(消息6)。节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_operator(消息7)。邻居节点Neighbor向节点Router回复有对应名字的带有数据key_operator的数据包(消息8)。节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_site(消息9)。邻居节点Neighbor把附带key_site的数据包发送给节点Router(消息10)。

节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求key_root密钥(消息11)。

最后，邻居节点Neighbor向节点Router携带数据为key_root的数据包(消息12)。

基于NLSR的安全模型场景，对要用到的公式X和密钥K进行定义，公式X为数据密钥集DK、验证密钥集VK和数据Data，密钥K为数据密钥集DK和验证密钥集VK，定义如下：

X∈DK∪VK∪{Data}

K∈DK∪VK

为了给出NLSR安全模型精简的理想化，只对所有数据包进行理想化(即消息2、消息 4、消息6、消息8、消息10和消息12)，并只保留其中的内容部分和签名部分，因为这两者是涉及到加密解密，从而可以使用改进的BAN逻辑得到如下理想化结果。

对消息2的LSA数据包进行理想化得到：

M1.1：

M1.2：

M1.3：

M1.4：

M1.5：

M1.6：

消息4、消息6、消息8、消息10和消息12携带密钥的数据包进行理想化得到：

M2：RΔ(key_NLSR)_c

M3：RΔ(key_router)_c

M4：RΔ(key_operator)_c

M5：RΔ(key_site)_c

M6：RΔ(key_root)_c

首先根据已知安全模型，对数据密钥的基础信息给出初始化假设定义。

定义DK＝{key_NLSR}，VK＝{key_router，key_operater，key_site，key_root}。

同时定义假设集合如下：

A1：

其中key∈DK∪VK

A2：RΔkey→R|≡＃key，其中key∈DK∪VK

A3：N|≈key，其中key∈DK∪VK

A4：RΔData→R|≡＃Data

A5：

(3)验证模型的数据安全目标和密钥安全目标

同时针对NLSR安全模型的形式化模型，提取需要验证的两种安全目标，一个是数据安全目标即保证读者收到了数据、读者相信邻居节点相信数据为真，同时读者相信数据为真，另一个是密钥安全目标即保证读者收到了所有密钥，读者相信邻居相信所有密钥为真，同时读者相信所有密钥为真。

使用BAN- n逻辑，对数据安全目标进行理想化表达，需要验证：

G1：RΔData

G2：R|≡N|≡Data

G3：R|≡Data

使用BAN- n逻辑，对数据安全目标进行理想化表达，对于key∈KEY需要验证：

G4：RΔkey

G5：R|≡N|≡key

G6：R|≡key

证明过程：

通过把看见规则SEE3应用于消息M1.1得到：

S1：

把看见规则SEE4应用于消息M1.2-M1.5会得到：

S2：

S3：

S4：

S5：

S6：

通过把看见规则SEE5应用于消息M2-M6会得到：

S7：RΔkey_NLSR

S8：RΔkey_router

S9：RΔkey_operator

S10：RΔkey_site

S11：RΔkey_root

将分离规则(MP)应用于S7-S11和假设A1来获得：

S12：

S13：

S14：

S15：

S16：

将验证密钥规则KV1应用于S3、S14和消息M3得到：

S17：R|≈key_router

将验证密钥规则KV1应用于S4、S15和消息M4得到：

S18：R|≈key_operator

将验证密钥规则KV1应用于S5、S16和消息M5得到：

S19：R|≈key_site

将验证密钥规则KV1应用于S6、S16和消息M6会得到：

S20：R|≈key_root

将验证密钥规则KV2应用于S17-S20、S2和S12得到：

S21：R|≈key_NLSR

将看见规则SEE2应用于S1和S12可以得到：

S22：RΔData

将分离规则(MP)应用于S22和假设A4得到：

S23：R|≡＃Data

将消息含义规则MM1应用于S12、S1和S21得到：

S24：R|≡N|～Data

将临时值验证规则NV应用于S23和S24得到：

S25：R|≡N|≡Data

把管辖规则J应用于假设A5和S25得到：

S26：R|≡Data

把分离规则(MP)应用于S7-S11和假设A2得到：

S27：R|≡＃key_NLSR

S28：R|≡＃key_router

S29：R|≡＃key_operator

S30：R|≡＃key_site

S31：R|≡＃key_root

把管辖权验证规则JV应用于假设A4、S17-S21和S7-S11可得：

S32：

S33：

S34：

S35：

S36：

把消息含义规则MM1应用于S2、S13和S17得到：

S37：R|≡N|～key_NLSR

把消息含义规则MM1应用于S3、S14和S18得到：

S38：R|≡N|～key_router

把消息含义规则MM1应用于S4、S15和S19得到：

S39：R|≡N|～key_operator

把消息含义规则MM1应用于S5、S16和S20得到：

S40：R|≡N|～key_site

把消息含义规则MM1应用于S6、S16和S20得到：

S41：R|≡N|～key_root

把临时值验证规则NV应用于S27-S31和S37-S41可以得到：

S42：R|≡N|≡key_NLSR

S43：R|≡N|≡key_router

S44：R|≡N|≡key_operator

S45：R|≡N|≡key_site

S46：R|≡N|≡key_root

将管辖规则J应用于S32-S36和S42-S46得到：

S47：R|≡key_NLSR

S48：R|≡key_router

S49：R|≡key_operator

S50：R|≡key_site

S51：R|≡key_root

S22、S25和S26分别对应了数据安全性目标G1、G2和G3，因此数据安全性目标得到了验证。S7-S11、S42-S46和S47-S51分别对应了密钥安全目标G4、G5和G6，因此密钥安全目标得到了验证。

(4)使用BAN- n逻辑对NLSR安全模型(带入侵者)进行建模

通过对带有入侵者的安全模型的分析，这里只考虑前四步有入侵者Intruder伪造消息的情况，前四步与节点Router进行通信的是入侵者Intruder，而节点Router误以为Intruder是邻居节点Neighbor，抽取出了当前节点Router和邻居节点Neighbor的LSA 数据包收发过程，如附图4所示。

附图4中节点之间的LSA数据包收发过程，可以写为如下12条消息：

消息1′.Router-＞Neighbor(Intruder)：name_Data

消息2′.Neighbor(Intruder)-＞Router：

消息3′.Router-＞Neighbor(Intruder)：

消息4′.Neighbor(Intruder)-＞Router：

key_{NLSR_fake}

消息5.Router-＞Neighbor：

消息6.Neighbor-＞Router：

key_router

消息7.Router-＞Neighbor：

消息8.Neighbor-＞Router：

key_operator

消息9.Router-＞Neighbor：

消息10.Neighbor-＞Router：

key_site

消息11.Router-＞Neighbor：

消息12.Neighbor-＞Router：

key_root

首先，Router向Inturder假冒的邻居节点发送LSA的Interest包，包括了对应LSA的Data包的名字(消息1′)；Inturder假冒邻居节点Neighbor向节点Router发送LSA 数据包，包括数据名部分、数据部分、签名部分和签名信息部分。数据名部分包括name_Data，数据部分包括由私钥

签名部分包括

签名信息部分包括

(消息2′)；其次，节点Router向Inturder假冒的邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_{NLSR_fake}(消息3′)。然后，Inturder假冒邻居节点Neighbor向节点Router 回复有对应名字的带有数据key_{NLSR_fake}的数据包(消息4′)。节点Router向邻居节点 Neighbor发送名字为

的兴趣包，即请求密钥key_router(消息5)。之后，邻居节点Neighbor向节点Router回复有对应名字的带有数据key_router的数据包(消息6)。节点 Router向邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_operator(消息7)。邻居节点Neighbor向节点Router回复有对应名字的带有数据key_operator的数据包 (消息8)。节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求密钥key_site(消息9)。邻居节点Neighbor把附带key_site的数据包发送给节点Router(消息 10)。节点Router向邻居节点Neighbor发送名字为

的兴趣包，即请求key_root密钥(消息11)。最后，邻居节点Neighbor向节点Router携带数据为key_root的数据包(消息12)。

基于带入侵者的NLSR安全模型场景，重新对公式X和密钥K进行定义，公式X为数据密钥集DK、验证密钥集VK、伪造数据Data_fake和伪造的NLSR密钥key_{NLSR_fake}，密钥K为数据密钥集DK、验证密钥集VK和伪造的NLSR密钥key_{NLSR_fake}，定义如下：

X∈DK∪VK∪{Data_fake，key_{NLSR_fake}}

K∈DK∪VK∪{Data_fake}

为了给出带入侵者的NLSR安全模型精简的理想化，我们只对所有数据包进行理想化 (即消息2′、消息4、消息6、消息8、消息10和消息12)，并只保留其中的内容部分和签名部分，因为这两者是涉及到加密解密，从而可以使用改进的BAN逻辑得到如下理想化结果。

对消息2的LSA数据包进行理想化得到：

M1.1′：

M1.2：

M1.3：

M1.4：

M1.5：

M1.6：

对消息4′、消息6、消息8、消息10和消息12携带密钥的数据包进行理想化得到：

M2′：RΔ(key_{NLSR_fake})_c

M3：RΔ(key_router)_c

M4：RΔ(key_operator)_c

M5：RΔ(key_site)_c

M6：RΔ(key_root)_c

(5)验证模型的伪造数据入侵目标和伪造密钥入侵目标

同时针对带有入侵者的NLSR安全模型的形式化模型，继续验证伪造数据入侵目标和伪造密钥入侵目标。

使用BAN- n逻辑，需要完成验证的伪造数据入侵目标如下：

G7：RΔData_fake

G8：R|≡N|≡Data_fake

G9：R|≡Data_fake

使用BAN- n逻辑，需要完成验证的伪造密钥入侵目标如下：

G10：RΔkey_{NLSR_fake}

G11：R|≡N|≡key_{NLSR_fake}

G12：R|≡key_{NLSR_fake}

证明过程：

通过把看见规则SEE3应用于消息M1.1得到：

S1′：

通过把看见规则SEE4应用于消息M1.2-M1.5会得到：

S2′：

S3：

S4：

S5：

S6：

通过把看见规则SEE5应用于消息M2-M6会得到：

S7′：RΔkey_{NLSR_fake}

S8：RΔkey_router

S9：RΔkey_operator

S10：RΔkey_site

S11：RΔkey_root

将分离规则(MP)应用于消息S7′-S11和假设A1来获得：

S12′：

S13：

S14：

S15：

S16：

将验证密钥规则KV1应用于S3、S14和消息M3得到：

S17：R|≈key_router

将验证密钥规则KV1应用于S4、S15和消息M4得到：

S18：R|≈key_operator

将验证密钥规则KV1应用于S5、S16和消息M5得到：

S19：R|≈key_site

将验证密钥规则KV1应用于S6、S16和消息M6得到：

S20：R|≈key_root

因为不存在

无法使用验证密钥规则KV2得到S21′：R|≈key_{NLSR_fake}。

将看见规则SEE1应用于S1和S12可以得到：

S22：RΔData_fake

将分离规则(MP)应用于S22和假设A4得到：

S23：R|≡＃Data_fake

同时由于没有S21′，无法将消息含义规则MM1应用于S1、S12和S21′得到：

S24′：R|≡N|～Data_fake

同时也无法将临时值验证规则NV应用于S23和S24′得到：

S25′：R|≡N|≡Data_fake

也无法把管辖规则J应用于假设A5和S25′得到：

S26′：R|≡Data_fake

由于仅仅可以得到S22对应伪造数据入侵目标G7，而无法得到S25′和S26′对应伪造数据入侵目标G8和G9。因此无法完成伪造数据入侵目标的证明，即入侵者无法成功用伪造数据欺骗reader。

把分离规则(MP)应用于S7′-S11和假设A1得到：

S27′：R|≡＃key_{NLSR_fake}

S28：R|≡＃key_router

S29：R|≡＃key_operator

S30：R|≡＃key_site

S31：R|≡＃key_root

由于没有S21′：R|≈key_{NLSR_fake}因此无法使用管辖权验证规则JV应用于假设A4、S21′和S7′得到S32′：

同时由于没有S21′，无法将消息含义规则MM1应用于S2、S13和S21′得到：

S37′：R|≡N|～key_{NLSR_fake}

进而由于没有S37′，无法把临时值验证规则NV应用于S27′和S37′得到：

S42′：R|≡N|≡key_{NLSR_fake}

也由于没有S37′和S42′，无法将管辖规则J应用于S37′和S42′得到：

S47′：R|≡key_{NLSR_fake}

由于仅仅可以得到S7对应伪造密钥入侵目标G10，而无法得到S42′和S47′对应伪造数据入侵目标G11和G12。因此无法完成伪造密钥入侵目标的证明，即入侵者无法成功用伪造密钥欺骗reader。

综上所述，通过BAN- n逻辑对NLSR安全模型的应用，完成了对该NLSR安全模型的安全分析和验证。该模型具有BAN逻辑的推理规则简单明了，使用方便，并可以被验证保证数据安全目标和密钥安全目标，同时能保证在有入侵者的情况下，入侵者无法用伪造密钥和伪造数据来完成入侵，即验证了伪造数据入侵目标和伪造密钥入侵目标。BAN- n逻辑可以被应用于更多命名数据网络相关的协议上，具有可拓展性，有利于提高在现实生活中协议具体实现时的鲁棒性，为个人隐私安全保驾护航。