密码协议形式化分析与可证明安全实验1——使用proverif来分析密码协议

2024-03-28 09:59
文章标签 分析 使用 协议 安全 实验 密码 证明 形式化 proverif

本文主要是介绍密码协议形式化分析与可证明安全实验1——使用proverif来分析密码协议，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

配置ProVerif环境

实验环境： Windows 11 X64
根据ProVerif用户手册1.4.3节，Windows用户可以使用二进制发行版安装ProVerif。首先现在你想要的文件路径中新建一个proverif文件夹。

相关依赖组件安装

graphviz

graphviz是一种以图形方式显示ProVerif可能发现攻击的组件，可以通过官网链接进行下载。
在这里插入图片描述
我的操作系统是64位系统，所以我选择64位的 EXE installer。
下载后将其解压到解压到proverif文件中。
接下来配置环境变量，配置路径：控制面板->系统->高级系统设置->环境变量。
在这里插入图片描述

在这里插入图片描述
在命令行窗口中输入dot -version查看是否已经安装成功，出现以下内容则已经安装成功。
在这里插入图片描述

GTK+2.24(可选)

如果要运行交互式模拟器proverif交互，则需要安装GTK+2.24，也可以通过官网链接进行下载。
在这里插入图片描述
同样下载适配我的电脑的版本。下载完之后是一个压缩包：gtk+-bundle_2.24.10-20120208_win32.zip，解压到proverif文件中，将解压文件改名为GTK。
同样对其进行环境配置，配置路径：控制面板->系统->高级系统设置->环境变量。
在这里插入图片描述

ProVerif安装

Windows二进制包proverifbin2.05.tar.gz从以下老的不行的官网链接进行下载。
在这里插入图片描述
下载之后将它放到之前建好的proverif文件夹中，我们使用以下命令行窗口来解压。

	cd /d D:\proveriftar -zxvf proverif2.05.tar.gz

解压完成后，proverif文件夹就会出现一个名为proverif2.05的文件。
在这里插入图片描述

测试

在proverif2.05文件中新建一个txt文件，输入以下内容：

free c:channel.free Cocks:bitstring[private].
free RSA:bitstring[private].query attacker(RSA).
query attacker(Cocks).processout(c,RSA);0

命名为hello.pv（记得修改文件后缀名，不然会不成功）。
在命令行窗口中输入proverif hello.pv，出现以下内容即成功。
在这里插入图片描述

HandShake Protocol握手协议

(* Symmetric key encryption *)type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.(* Asymmetric key encryption *)type skey.
type pkey.fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.(* Digital signatures *)type sskey.
type spkey.fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.free c:channel.free s:bitstring [private].
query attacker(s).let clientA(pkA:pkey,skA:skey,pkB:spkey) =out(c,pkA);in(c,x:bitstring);let y = adec(x,skA) inlet (=pkB,k:key) = checksign(y,pkB) inout(c,senc(s,k)).let serverB(pkB:spkey,skB:sskey) =in(c,pkX:pkey);new k:key;out(c,aenc(sign((pkB,k),skB),pkX));in(c,x:bitstring);let z = sdec(x,k) in0.processnew skA:skey;new skB:sskey;let pkA = pk(skA) in out(c,pkA);let pkB = spk(skB) in out(c,pkB);( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB)) )

协议分析

这里首先分析一下上面的代码的工作，proverif从process标记的主进程开始分析，所以这里看process后面的内容。

首先是为clientA生成了非对称加密私钥skA，同时为serverB生成了签名用的私钥skB，并分别为这两个私钥生成对应的公钥（pkA，pkB），并通过公开信道c将这两个公钥发送出去。

接下来调用两个进程宏clientA和serverB来实现两个进程的并发执行，这里用replication的方式让两个主体都以无限数量会话并发执行（clientA和serverB前面的感叹号表示重复无限多个会话并发）。

然后关注clientA和serverB这两个模块，这里要把两个模块结合起来看，首先是A把自己公钥pkA发出去，B会接收到这个公钥pkX，同时创建一个对称密钥k（k这里起到临时会话密钥的作用）。

然后B将这个临时密钥k和自己的公钥pkB一起打包成元组，先用自己的私钥skB签名（sign部分），再用收到的公钥pkX加密，并通过公共信道发出去（aenc部分，这里aenc表示非对称加密）。

A通过信道接收到这个发来的bitstring，然后用自己私钥解密，解密成功之后得到y，之后用B的公钥pkB验证签名，如果验证通过了就会得到元组(m,k)，第一项就是pkB（这里用=pkB来匹配），第二项就是对称密钥kA再用这个k给消息s进行对称加密然后发出去，B接收到发来的bitstring之后，用自己刚刚创建的对称密钥k解密就得到了内容z，这应该和s是一样的内容

不难看出，这段代码很简单，所以也不难想到中间人攻击。

proverif协议分析

将上述代码保存为ex_handshake.pv文件，然后执行以下命令，可以得到proverif分析上述握手协议的结果。

proverif ex_handshake.pv

ProVerif会输出其考虑过程的内部表示，然后一次处理逻辑中的查询（由query关键字表示），查询攻击者的输出可以分为三个部分:

  • Abbreviations到detailsed部分：proverif推导出的导致攻击的流程
  • detailed到trace has been found：描述了上述攻击的轨迹
  • result：最终结论，true表示不存在攻击，false表示存在攻击者获取相关信息

这里分部分来看，首先是abbreviations的部分：
在这里插入图片描述
在这里插入图片描述
在这里插入图片描述

  1. attacker用一个已知的私钥 k_3 生成对应的公钥 pk(k_3) （对应abbreviations的前两步，这里的k_3 可以是attacker自己生成的，或者通过其他方式已知的）。
  2. 然后这里标记了代码的{16}位置，该位置表示可以从信道中收到攻击者发出的公钥 pk(k_3) ，同时在{18}位置会将消息aenc(sign((spk(skB[]),k_2),skB[]),pk(k_3)) 消息通过信道发出，此时
    attacker可以接收到这条消息（也即attacker获取到了这个知识）。
  3. 然后attacker可以从信道中获得这条加密的消息（ aenc ），attacker利用私钥 k_3 对其解密，可以得到 sign((spk(skB[],k_2),skB[])) ，并通过 getmess 获取签名的内容（也即(spk(skB[]),k_2) ），这里意味着attacker可以获得 k_2。
  4. 之后attacker获取A的公钥 pkA ，并用该公钥对sign((spk(skB[]),k_2),skB[]) 进行加密并发送出去。
  5. 这条消息会在{10}被client收到，client验证签名政确之后，会在{13}将消息 senc(s[],k_2) 发送出去，attacker会收到这条消息。
  6. 之后attacker就可以用 k_2 解密得到 s[]。

然后看detailed output的部分
在这里插入图片描述

  • 前两行对应的是公钥密钥对和签名密钥对的创建过程。
  • 然后是三个out，前两个out表示attacker将加密公钥和签名公钥分别保存在 ~M 和 ~M_1 中，第三个out表示client在{9}处的输出，attacker将其保存为 ~M_2。
  • 从下面开始，之后的每一行后面都跟了一个 in copy a 或者 in copy a_2 ，相同的标识表示相同的会话， copy a 表示当前attacker正在与client进行通信， copy a_2 表示当前attacker正在和server通信
  • 接下来，表示attacker向server发送了一个公钥，同时server返回了一个用server私钥签名并加密的消息，这里attacker将这条消息保存为 ~M_3。
  • 然后，里表示attacker在{10}这里，用 a_1 这个私钥解密 ~M_3 ，再用client的公钥加密（这里的 ~M 就是client的公钥），将加密后的消息发送出去，当client在{13}返回加密的消息时，attacker可以利用 k_4 解密并获得 s。

那么我们对该协议进行改进，在协议中加入对认证性的验证：

(* 客户端认为自己在使用key对称密钥和服务器进行协议交互 *)
event acceptsClient(key).
(* 服务器认为自己在使用key对称密钥和pkey公钥标识的客户端进行协议交互 *)
event acceptsServer(key,pkey).
(* pkey标识的客户端认为自己使用key和服务器进行协议交互结束 *)
event termClient(key,pkey).
(* 服务器认为自己使用key对称密钥和客户端进行协议交互结束 *)
event termServer(key).(* 对于每个以对称密钥x和服务器交互结束的客户端y前面总是存在认定以对称密钥x和客户端y交互的服务器 *)
query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).
(* 对于每个以对称密钥x交互结束的服务器前面总是存在一个区别于其它的“以对称密钥x和服务器交互的客户端”即单射关系 *)
query x:key; inj-event(termServer(x))==>inj-event(acceptsClient(x)).

完整的协议如下：

(* Symmetric key encryption *)type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.(* Asymmetric key encryption *)type skey.
type pkey.fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.(* Digital signatures *)type sskey.
type spkey.fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.free c:channel.free s:bitstring [private].
query attacker(s).event acceptsClient(key).
event acceptsServer(key,pkey).
event termClient(key,pkey).
event termServer(key).query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).
query x:key; inj-event(termServer(x))==>inj-event(acceptsClient(x)).let clientA(pkA:pkey,skA:skey,pkB:spkey) = out(c,pkA);in(c,x:bitstring); let y = adec(x,skA) inlet (=pkB,k:key) = checksign(y,pkB) in(* 客户端解密成功+验证成功后即认为接受了使用密钥k通信 *)event acceptsClient(k);out(c,senc(s,k));(* 客户端运行结束，本次是使用k通信，自己的公钥是pkA *)event termClient(k,pkA).let serverB(pkB:spkey,skB:sskey,pkA:pkey) = in(c,pkX:pkey);new k:key; (* 服务器收到客户端公钥pkX，并创建了密钥k，即认为接受了使用密钥k和客户端pkX通信 *)event acceptsServer(k,pkX);out(c,aenc(sign((pkB,k),skB),pkX));in(c,x:bitstring); let z = sdec(x,k) in(* 如果接收到的pkX确实是pkA，即认为服务器使用对称密钥k运行结束 *)if pkX = pkA then event termServer(k).process new skA:skey; new skB:sskey;let pkA = pk(skA) in out(c,pkA);let pkB = spk(skB) in out(c,pkB);( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB,pkA)) )

这一版只是加了认证性质的验证，但是还是没有解决中间人攻击问题。
在这里插入图片描述
结果第一条表明，对消息s还是不满足安全性的。

结果第二条表明，从B（服务器）到A（客户端）的认证是不满足的，也就是说如果客户端觉得自己和服务器完成了协议流程，不一定真的有这个服务器在和客户端走协议，这个也是因为中间人可以冒充服务器来和客户端通信。

结果第三条表明，从A（客户端）到B（服务器）的认证是满足的，也就是说如果服务器觉得自己走完了协议流程，一定至少有一个客户端是在和自己走协议的。

所以我们需要进步以改进这个协议，让服务器回传的信息中包含客户端的标识来防止中间人攻击的发生。

type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.free c:channel.
free s:bitstring [private].
query attacker(s).event acceptsClient(key).
event acceptsServer(key,pkey).
event termClient(key,pkey).
event termServer(key).query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).
query x:key; inj-event(termServer(x))==>inj-event(acceptsClient(x)).let clientA(pkA:pkey,skA:skey,pkB:spkey) = out(c,pkA);in(c,x:bitstring); let y = adec(x,skA) in(* 这里检查一下这个包确实是要发给自己pkA的 *)let (=pkA,=pkB,k:key) = checksign(y,pkB) inevent acceptsClient(k);out(c,senc(s,k));event termClient(k,pkA).let serverB(pkB:spkey,skB:sskey,pkA:pkey) = in(c,pkX:pkey);new k:key; event acceptsServer(k,pkX);(* 这里把要通信的客户端标识pkX放进去 *)out(c,aenc(sign((pkX,pkB,k),skB),pkX));in(c,x:bitstring); let z = sdec(x,k) inif pkX = pkA then event termServer(k).process new skA:skey; new skB:sskey;let pkA = pk(skA) in out(c,pkA);let pkB = spk(skB) in out(c,pkB);( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB,pkA)) )

现在三条性质都能验证通过。
在这里插入图片描述

Needham-Schroeder Protocol

Needham-Schroeder认证协议，是一种多次提问——响应协议，可以对付重放攻击。每一个会话回合都有一个新的随机数在起作用。
在这里插入图片描述

  1. A 向KDC 发送报文1，表明要与B通信。KDC以报文2回答。报文1中加入了由A 指定的随机数R_A, KDC 的回答报文中也有R_A, 它的这个作用是保证报文2是新鲜的，而不是重放的。
  2. 报文2中的K_B(A, K_S) 是KDC 交给A 的入场券，其中有KDC 指定的会话键K_S, 并且用B和KDC 之间的密钥加密，A 无法打开，只能原样发给B。

下面给出Needham-Schroeder 密钥共享协议的三个变体，说明各个协议变体存在的缺陷，尝试给出攻击方式。

NeedhamSchroederPK-var1.pv

free c: channel.(* Public key encryption *)
type pkey.
type skey.fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; adec(aenc(x, pk(y)),y) = x.(* Signatures *)
type spkey.
type sskey.fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall x: bitstring, y: sskey; getmess(sign(x,y)) = x.
reduc forall x: bitstring, y: sskey; checksign(sign(x,y), spk(y)) = x.(* Shared key encryption *)
fun senc(bitstring,bitstring): bitstring.
reduc forall x: bitstring, y: bitstring; sdec(senc(x,y),y) = x.
(* Authentication queries *)
event beginBparam(pkey).
event endBparam(pkey).
event beginAparam(pkey).
event endAparam(pkey).query x: pkey; inj-event(endBparam(x)) ==> inj-event(beginBparam(x)).
query x: pkey; inj-event(endAparam(x)) ==> inj-event(beginAparam(x)).(* Secrecy queries *)
free secretANa, secretANb, secretBNa, secretBNb: bitstring [private].query attacker(secretANa);attacker(secretANb);attacker(secretBNa);attacker(secretBNb).(* Alice *)
let processA(pkB: pkey, skA: skey) =in(c, pkX: pkey);event beginBparam(pkX); new Na: bitstring; out(c, aenc((Na, pk(skA)), pkX));in(c, m: bitstring); let (=Na, NX: bitstring) = adec(m, skA) inout(c, aenc(NX, pkX));if pkX = pkB  thenevent endAparam(pk(skA));out(c, senc(secretANa, Na));out(c, senc(secretANb, NX)).(* Bob *)
let processB(pkA: pkey, skB: skey) =in(c, m: bitstring);let (NY: bitstring, pkY: pkey) = adec(m, skB) inevent beginAparam(pkY);new Nb: bitstring;out(c, aenc((NY, Nb), pkY));in(c, m3: bitstring);if Nb = adec(m3, skB) thenif pkY = pkA thenevent endBparam(pk(skB));out(c, senc(secretBNa, NY));out(c, senc(secretBNb, Nb)).(* Main *)
process new skA: skey; let pkA = pk(skA) in out(c, pkA);new skB: skey; let pkB = pk(skB) in out(c, pkB);( (!processA(pkB, skA)) | (!processB(pkA, skB)) )

使用proverif分析结果

在这里插入图片描述

  1. 这个查询表示当B的参数结束时，相应的B的参数开始是否受到注入攻击。由于结果是false，说明在这个情况下，检测到乐注入攻击。

  2. 这个查询表示当A的参数结束时，相应的A的参数开始是否受到注入攻击。由于结果是true，说明在这个情况下，没有检测到注入攻击。

  3. 这个查询表示攻击者是否能够获得A的某个密钥（可能是Na）。结果是true，说明攻击者无法获取此密钥

  4. 这个查询类似于上一个，表示攻击者是否能够获得A的另一个密钥。结果是true，说明攻击者无法获取此密钥。

  5. 这个查询表示攻击者是否能够获得B的某个密钥（可能是Na）。结果是false，说明攻击者能够获取此密钥。

  6. 这个查询类似于上一个，表示攻击者是否能够获得B的另一个密钥。结果是false，说明攻击者能够获取此密钥。

漏洞分析

注入攻击检测不完善

查询 inj-event(endBparam(x)) ==> inj-event(beginBparam(x)) is false 表明系统在B参数结束时未能检测到注入攻击。这可能意味着系统对于某些情况下的注入攻击检测不够强大，需要进一步改进。

密钥泄漏问题

查询 not attacker(secretBNa[]) is false 和 not attacker(secretBNb[]) is false 表明攻击者能够获取B的某些密钥。这可能是系统中的一个重大漏洞，需要加强密钥管理和保护机制，以防止攻击者获取关键信息。

部分成功的注入攻击

查询 inj-event(endAparam(x)) ==> inj-event(beginAparam(x)) is true 表明系统在A参数结束时检测到了注入攻击。这可能表示在某些情况下系统能够成功地检测到攻击，但在其他情况下可能会失败。需要深入研究系统在各种场景下的注入攻击检测能力。

部分密钥保护

查询 not attacker(secretANa[]) is true 和 not attacker(secretANb[]) is true 表明攻击者无法获取A的某些密钥。这是系统的一个积极方面，但仍然需要确保所有关键密钥都得到足够的保护。

NeedhamSchroederPK-var2.pv

free c: channel.(* Public key encryption *)
type pkey.
type skey.fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; adec(aenc(x, pk(y)),y) = x.(* Signatures *)
type spkey.
type sskey.fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall x: bitstring, y: sskey; getmess(sign(x,y)) = x.
reduc forall x: bitstring, y: sskey; checksign(sign(x,y), spk(y)) = x.(* Shared key encryption *)
type nonce.fun senc(bitstring,nonce): bitstring.
reduc forall x: bitstring, y: nonce; sdec(senc(x,y),y) = x.(* Type converter *)
fun nonce_to_bitstring(nonce): bitstring [data,typeConverter].(* Two honest host names A and B *)
type host.
free A, B: host.(* Key table *)
table keys(host, pkey).(* Authentication queries *)
event beginBparam(host).
event endBparam(host).
event beginAparam(host).
event endAparam(host).query x: host; inj-event(endBparam(x)) ==> inj-event(beginBparam(x)).
query x: host; inj-event(endAparam(x)) ==> inj-event(beginAparam(x)).(* Secrecy queries *)
free secretANa, secretANb, secretBNa, secretBNb: bitstring [private].query attacker(secretANa);attacker(secretANb);attacker(secretBNa);attacker(secretBNb).(* Alice *)
let processA(pkS: spkey, skA: skey) =in(c, hostX: host);event beginBparam(hostX); 		out(c, (A, hostX));                              (* msg 1 *)in(c, ms: bitstring);                            (* msg 2 *)let (pkX: pkey, =hostX) = checksign(ms, pkS) innew Na: nonce; out(c, aenc((Na, A), pkX));                      (* msg 3 *)in(c, m: bitstring);                             (* msg 6 *)let (=Na, NX: nonce) = adec(m, skA) inout(c, aenc(nonce_to_bitstring(NX), pkX));       (* msg 7 *)if hostX = B thenevent endAparam(A);out(c, senc(secretANa, Na));out(c, senc(secretANb, NX)).(* Bob *)
let processB(pkS: spkey, skB: skey) =in(c, m: bitstring);                             (* msg 3 *)let (NY: nonce, hostY: host) = adec(m, skB) inevent beginAparam(hostY);out(c, (B, hostY));                              (* msg 4 *)in(c,ms: bitstring);                             (* msg 5 *)let (pkY: pkey,=hostY) = checksign(ms, pkS) innew Nb: nonce;out(c, aenc((NY, Nb), pkY));                     (* msg 6 *)in(c, m3: bitstring);                            (* msg 7 *)if nonce_to_bitstring(Nb) = adec(m3, skB) thenif hostY = A thenevent endBparam(B);out(c, senc(secretBNa, NY));out(c, senc(secretBNb, Nb)).(* Trusted key server *)
let processS(skS: sskey) =  in(c,(a: host, b: host)); get keys(=b, sb) inout(c,sign((sb,b), skS)).(* Key registration *)
let processK =in(c, (h: host, k: pkey));if h <> A && h <> B then insert keys(h,k).(* Main *)
process new skA: skey; let pkA = pk(skA) in out(c, pkA); insert keys(A, pkA);new skB: skey; let pkB = pk(skB) in out(c, pkB); insert keys(B, pkB);new skS: sskey; let pkS = spk(skS) in out(c, pkS);( (!processA(pkS, skA)) | (!processB(pkS, skB)) | (!processS(skS)) | (!processK) )

使用proverif分析结果

在这里插入图片描述

漏洞分析

同NeedhamSchroederPK-var1.pv

NeedhamSchroederPK-var3.pv

(* Loops if types are ignored *)
set ignoreTypes = false.free c: channel.type host.
type nonce.
type pkey.
type skey.
type spkey.
type sskey.fun nonce_to_bitstring(nonce): bitstring [data,typeConverter].(* Public key encryption *)
fun pk(skey): pkey.
fun encrypt(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; decrypt(encrypt(x,pk(y)),y) = x.(* Signatures *)
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, k: sskey; getmess(sign(m,k)) = m.
reduc forall m: bitstring, k: sskey; checksign(sign(m,k), spk(k)) = m.(* Shared key encryption *)
fun sencrypt(bitstring,nonce): bitstring.
reduc forall x: bitstring, y: nonce; sdecrypt(sencrypt(x,y),y) = x.(* Secrecy assumptions *)
not attacker(new skA).
not attacker(new skB).
not attacker(new skS).(* 2 honest host names A and B *)
free A, B: host.table keys(host, pkey).(* Queries *)
free secretANa, secretANb, secretBNa, secretBNb: bitstring [private].
query attacker(secretANa);attacker(secretANb);attacker(secretBNa);attacker(secretBNb).event beginBparam(host, host).
event endBparam(host, host).
event beginAparam(host, host).
event endAparam(host, host).
event beginBfull(host, host, pkey, pkey, nonce, nonce).
event endBfull(host, host, pkey, pkey, nonce, nonce).
event beginAfull(host, host, pkey, pkey, nonce, nonce).
event endAfull(host, host, pkey, pkey, nonce, nonce).query x: host, y: host; inj-event(endBparam(x,y)) ==> inj-event(beginBparam(x,y)).query x1: host, x2: host, x3: pkey, x4: pkey, x5: nonce, x6: nonce; inj-event(endBfull(x1,x2,x3,x4,x5,x6))  ==> inj-event(beginBfull(x1,x2,x3,x4,x5,x6)).query x: host, y: host; inj-event(endAparam(x,y)) ==> inj-event(beginAparam(x,y)).query x1: host, x2: host, x3: pkey, x4: pkey, x5: nonce, x6: nonce; inj-event(endAfull(x1,x2,x3,x4,x5,x6)) ==> inj-event(beginAfull(x1,x2,x3,x4,x5,x6)).(* Role of the initiator with identity xA and secret key skxA *)
let processInitiator(pkS: spkey, skA: skey, skB: skey) =(* The attacker starts the initiator by choosing identity xA,and its interlocutor xB0.We check that xA is honest (i.e. is A or B)and get its corresponding key. *)in(c, (xA: host, hostX: host));if xA = A || xA = B thenlet skxA = if xA = A then skA else skB inlet pkxA = pk(skxA) in(* Real start of the role *)event beginBparam(xA, hostX); (* Message 1: Get the public key certificate for the other host *)out(c, (xA, hostX));(* Message 2 *)in(c, ms: bitstring); let (pkX: pkey, =hostX) = checksign(ms,pkS) in(* Message 3 *)new Na: nonce; out(c, encrypt((Na, xA), pkX));(* Message 6 *)in(c, m: bitstring); let (=Na, NX2: nonce) = decrypt(m, skxA) inevent beginBfull(xA, hostX, pkX, pkxA, Na, NX2);(* Message 7 *)out(c, encrypt(nonce_to_bitstring(NX2), pkX));(* OK *)if hostX = B || hostX = A thenevent endAparam(xA, hostX);event endAfull(xA, hostX, pkX, pkxA, Na, NX2);out(c, sencrypt(secretANa, Na));out(c, sencrypt(secretANb, NX2)).(* Role of the responder with identity xB and secret key skxB *)
let processResponder(pkS: spkey, skA: skey, skB: skey) =(* The attacker starts the responder by choosing identity xB.We check that xB is honest (i.e. is A or B). *)in(c, xB: host);if xB = A || xB = B thenlet skxB = if xB = A then skA else skB inlet pkxB = pk(skxB) in(* Real start of the role *)(* Message 3 *)in(c, m: bitstring);let (NY: nonce, hostY: host) = decrypt(m, skxB) inevent beginAparam(hostY, xB);(* Message 4: Get the public key certificate for the other host *)out(c, (xB, hostY));(* Message 5 *)in(c,ms: bitstring);let (pkY: pkey,=hostY) = checksign(ms,pkS) in(* Message 6 *)new Nb: nonce;event beginAfull(hostY, xB, pkxB, pkY, NY, Nb);out(c, encrypt((NY, Nb), pkY));(* Message 7 *)in(c, m3: bitstring);if nonce_to_bitstring(Nb) = decrypt(m3, skB) then(* OK *)if hostY = A || hostY = B thenevent endBparam(hostY, xB);event endBfull(hostY, xB, pkxB, pkY, NY, Nb);out(c, sencrypt(secretBNa, NY));out(c, sencrypt(secretBNb, Nb)).(* Server *)
let processS(skS: sskey) =  in(c,(a: host, b: host)); get keys(=b, sb) inout(c,sign((sb,b),skS)).(* Key registration *)
let processK =in(c, (h: host, k: pkey));if h <> A && h <> B then insert keys(h,k).(* Main *)
process new skA: skey; let pkA = pk(skA) in	out(c, pkA); insert keys(A, pkA);new skB: skey; let pkB = pk(skB) in out(c, pkB); insert keys(B, pkB);new skS: sskey; let pkS = spk(skS) in out(c, pkS);((* Launch an unbounded number of sessions of the initiator *)(!processInitiator(pkS, skA, skB)) | (* Launch an unbounded number of sessions of the responder *)(!processResponder(pkS, skA, skB)) |(* Launch an unbounded number of sessions of the server *)(!processS(skS)) |(* Key registration process *)(!processK))

使用proverif分析结果

在这里插入图片描述

  1. 这个查询表示攻击者无法获取A的某些比特串（Na）。结果是true，表明系统在防止攻击者获取A的某些敏感比特串方面是成功的。

  2. 类似于前一个查询，这个查询表示攻击者无法获取A的另一组比特串（Nb）。结果是true，表明系统在保护A的敏感比特串上是成功的。

  3. 这个查询表示攻击者能够获取B的某些比特串（Na）。结果是false，这是一个潜在的漏洞，系统可能需要改进B的比特串保护措施，以防止攻击者获取关键信息

  4. 类似于前一个查询，这个查询表示攻击者能够获取B的另一组比特串（Nb）。结果是false，系统可能需要改进B的比特串保护机制

  5. 这个查询表示，在B参数结束时的注入事件不会导致在B参数开始时的注入事件。结果是true，表明系统在B参数的结束处成功防止了注入攻击。

  6. 类似于前一个查询，这个查询表示在B的完整数据结束时的注入事件不会导致在B的完整数据开始时的注入事件。结果是true，表明系统在B的完整数据结束处成功防止了注入攻击。

  7. 这个查询表示，在A参数结束时的注入事件会导致在A参数开始时的注入事件。这意味着系统在A参数的结束处未能防止注入攻击，结果是false，系统可能需要加强对A参数的注入攻击检测和防护措施。

  8. 类似于前一个查询，这个查询表示在A的完整数据结束时的注入事件会导致在A的完整数据开始时的注入事件。结果是false，表明系统在A的完整数据结束处未能防止注入攻击。系统可能需要改进对A的完整数据的注入攻击检测和防护机制

漏洞分析

A参数注入漏洞

漏洞分析： 可能存在未经过充分验证和过滤的A参数输入，导致在A参数结束时的注入事件影响了A参数的开始。

攻击方法： 攻击者可能会尝试通过在A参数结束时注入恶意代码或数据，来影响A参数的开始，执行未授权的操作或者篡改系统状态。

B参数比特串保护不足

漏洞分析： 暗示攻击者能够获取B参数的某些比特串，可能意味着存在对B参数比特串的不充分保护。

攻击方法： 攻击者可能会尝试通过拦截或者篡改B参数的比特串，来绕过安全控制，获取敏感信息或者执行未授权的操作。

A完整数据注入漏洞

漏洞分析： 暗示在A的完整数据结束时的注入事件可能影响A的完整数据的开始，表明存在对A完整数据注入的不足防护。

攻击方法： 攻击者可能会试图通过在A完整数据结束时注入恶意数据，来影响A完整数据的开始，导致数据不一致或者执行不当操作。

B完整数据注入漏洞

漏洞分析： 表明在B的完整数据结束时的注入事件无法有效防止在B的完整数据开始时的注入事件，存在B完整数据注入漏洞。

攻击方法： 攻击者可能会尝试通过在B完整数据结束时注入恶意数据，来绕过防护，影响B完整数据的开始，导致数据不一致或者执行不当操作。

引用参考

https://blog.csdn.net/JingYan_Chan/article/details/133149371
https://lauzyhou.blog.csdn.net/article/details/116376508
https://blog.csdn.net/LiLiLiZuoBuKai/article/details/126676169?ops_request_misc=&request_id=&biz_id=102&utm_term=needham-schroeder%20%E5%8D%8F%E8%AE%AE%E5%88%86%E6%9E%90&utm_medium=distribute.pc_search_result.none-task-blog-2allsobaiduweb~default-6-126676169.142v99control&spm=1018.2226.3001.4187

这篇关于密码协议形式化分析与可证明安全实验1——使用proverif来分析密码协议的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！


http://www.chinasem.cn/article/855297。

相关文章

中文分词jieba库的使用与实景应用（一）

中文分词jieba库的使用与实景应用（一）

知识星球：https://articles.zsxq.com/id_fxvgc803qmr2.html 目录 一.定义： 精确模式（默认模式）： 全模式： 搜索引擎模式： paddle 模式（基于深度学习的分词模式）： 二 自定义词典 三.文本解析   调整词出现的频率 四. 关键词提取 A. 基于TF-IDF算法的关键词提取 B. 基于TextRank算法的关键词提取
阅读更多...
使用SecondaryNameNode恢复NameNode的数据

使用SecondaryNameNode恢复NameNode的数据

1）需求： NameNode进程挂了并且存储的数据也丢失了，如何恢复NameNode 此种方式恢复的数据可能存在小部分数据的丢失。 2）故障模拟 （1）kill -9 NameNode进程 [lytfly@hadoop102 current]$ kill -9 19886 （2）删除NameNode存储的数据（/opt/module/hadoop-3.1.4/data/tmp/dfs/na
阅读更多...
Hadoop数据压缩使用介绍

Hadoop数据压缩使用介绍

一、压缩原则 （1）运算密集型的Job，少用压缩 （2）IO密集型的Job，多用压缩 二、压缩算法比较 三、压缩位置选择 四、压缩参数配置 1）为了支持多种压缩/解压缩算法，Hadoop引入了编码/解码器 2）要在Hadoop中启用压缩，可以配置如下参数
阅读更多...
Makefile简明使用教程

Makefile简明使用教程

文章目录 规则makefile文件的基本语法：加在命令前的特殊符号：.PHONY伪目标: Makefilev1 直观写法v2 加上中间过程v3 伪目标v4 变量 make 选项-f-n-C Make 是一种流行的构建工具，常用于将源代码转换成可执行文件或者其他形式的输出文件(如库文件、文档等)。Make 可以自动化地执行编译、链接等一系列操作。 规则 makefile文件
阅读更多...
性能分析之MySQL索引实战案例

性能分析之MySQL索引实战案例

文章目录 一、前言二、准备三、MySQL索引优化四、MySQL 索引知识回顾五、总结 一、前言 在上一讲性能工具之 JProfiler 简单登录案例分析实战中已经发现SQL没有建立索引问题，本文将一起从代码层去分析为什么没有建立索引？ 开源ERP项目地址：https://gitee.com/jishenghua/JSH_ERP 二、准备 打开IDEA找到登录请求资源路径位置
阅读更多...
使用opencv优化图片（画面变清晰）

使用opencv优化图片（画面变清晰）

文章目录 需求影响照片清晰度的因素 实现降噪测试代码 锐化空间锐化Unsharp Masking频率域锐化对比测试 对比度增强常用算法对比测试 需求 对图像进行优化，使其看起来更清晰，同时保持尺寸不变，通常涉及到图像处理技术如锐化、降噪、对比度增强等 影响照片清晰度的因素 影响照片清晰度的因素有很多，主要可以从以下几个方面来分析 1. 拍摄设备 相机传感器：相机传
阅读更多...
pdfmake生成pdf的使用

pdfmake生成pdf的使用

实际项目中有时会有根据填写的表单数据或者其他格式的数据，将数据自动填充到pdf文件中根据固定模板生成pdf文件的需求 文章目录 利用pdfmake生成pdf文件1.下载安装pdfmake第三方包2.封装生成pdf文件的共用配置3.生成pdf文件的文件模板内容4.调用方法生成pdf 利用pdfmake生成pdf文件 1.下载安装pdfmake第三方包 npm i pdfma
阅读更多...
零基础学习Redis(10) -- zset类型命令使用

零基础学习Redis(10) -- zset类型命令使用

zset是有序集合，内部除了存储元素外，还会存储一个score，存储在zset中的元素会按照score的大小升序排列，不同元素的score可以重复，score相同的元素会按照元素的字典序排列。 1. zset常用命令 1.1 zadd  zadd key [NX | XX] [GT | LT]   [CH] [INCR] score member [score member ...]
阅读更多...
【测试】输入正确用户名和密码，点击登录没有响应的可能性原因

【测试】输入正确用户名和密码，点击登录没有响应的可能性原因

目录 一、前端问题 1. 界面交互问题 2. 输入数据校验问题 二、网络问题 1. 网络连接中断 2. 代理设置问题 三、后端问题 1. 服务器故障 2. 数据库问题 3. 权限问题： 四、其他问题 1. 缓存问题 2. 第三方服务问题 3. 配置问题 一、前端问题 1. 界面交互问题 登录按钮的点击事件未正确绑定，导致点击后无法触发登录操作。 页面可能存在
阅读更多...
客户案例：安全海外中继助力知名家电企业化解海外通邮困境

客户案例：安全海外中继助力知名家电企业化解海外通邮困境

1、客户背景 广东格兰仕集团有限公司（以下简称“格兰仕”），成立于1978年，是中国家电行业的领军企业之一。作为全球最大的微波炉生产基地，格兰仕拥有多项国际领先的家电制造技术，连续多年位列中国家电出口前列。格兰仕不仅注重业务的全球拓展，更重视业务流程的高效与顺畅，以确保在国际舞台上的竞争力。 2、需求痛点 随着格兰仕全球化战略的深入实施，其海外业务快速增长，电子邮件成为了关键的沟通工具。
阅读更多...

Copyright China编程 23002807@qq.com

沪ICP备2023033072号-2