配置ProVerif环境
实验环境：Windows 11 X64
根据ProVerif用户手册的1.4.3节，Windows用户可以使用二进制发行版安装ProVerif。首先，在所需的文件路径中创建一个provif文件夹。
相关依赖组件安装
graphviz
Graphviz 是一个以图形方式显示ProVerif 发现的可能攻击的组件，可以从官方网站上的链接下载。
我的操作系统是64位系统，所以我选择64位EXE安装程序。
下载后解压成provif文件。
接下来，配置环境变量：配置路径：控制面板>系统>高级系统设置>环境变量。
在命令行窗口中输入dot -version，检查是否安装成功。 如果显示以下内容，则说明安装成功。
GTK+2.24(可选)
交互式模拟器如果要交互式运行Proverif，则需要安装GTK+2.24。也可以从官方网站上的链接下载。
另请下载适合我电脑的版本。下载后会生成压缩包gtk+-bundle_2.24.10-20120208_win32.zip。将其解压为provif文件并将解压后的文件重命名为GTK。
另外，配置环境（配置路径：控制面板> 系统> 高级系统设置> 环境变量）。
ProVerif安装
Windows二进制包provrifbin2.05.tar.gz可以从以下旧官网链接下载：
下载后，将其放入您之前创建的provif文件夹中，并使用以下命令行窗口解压缩。
cd /d D:\\proverif
tar -zxvf Prorif2.05.tar.gz
解压完成后，provif文件夹中将出现一个名为proverif2.05的文件。
测试
在provif2.05文件中创建一个新的txt文件并输入以下内容：
免费c:频道。
免费Cocks:bitstring [私人]。
免费RSA: 位串[私人]。
查询攻击者(RSA)。
查询攻击者（Cocks）。
过程
输出（c，RSA）；
0
将其命名为hello.pv（不要忘记更改文件的后缀，否则会失败）。
如果在命令行窗口中输入provif hello.pv，出现以下内容则说明成功。
HandShake Protocol握手协议
(* 对称密钥加密*)
输入密码。
fun senc(bitstring, key): 位串；
减少所有m: 位串、k: 键。 sdec(senc(m,k),k)=m。
(*非对称密钥加密*)
类型滑雪。
输入“pkey”。
有趣的pk(skey): pkey。
有趣的aenc(bitstring, pkey): 位字符串。
减少所有m:位串，sk: skey。 adec(aenc(m,pk(sk)),sk)=m.
（*电子签名*）
输入“sskey”。
键入spkey。
有趣的spk(sskey): spkey。
有趣的符号（位串，sskey）:位串。
减少所有m: 位串，ssk: sskey getmess(sign(m,ssk))=m。
减少所有m:位串，ssk: sskey。 checksign(sign(m,ssk),spk(ssk))=m.
免费c:频道。
免费s:bitstring [私人]。
查询攻击者。
让clientA(pkA:pkey,skA:skey,pkB:spkey)=
输出（c，pkA）；
in(c,x: 位串);
设y=adec(x,skA)
让(=pkB,k:key)=checksign(y,pkB) in
输出（c，senc（s，k））。
letserverB(pkB:spkey,skB:sskey)=
在（c，pkX:pkey）；
新k:key；
输出（c，aenc（符号（（pkB，k），skB），pkX））;
in(c,x: 位串);
设z=sdec(x,k)
0。
过程
新skA:skey；
新skB:sskey；
令pkA=pk(skA) in out(c,pkA);
pkB=spk(skB) in out(c,pkB);
( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB)) )
协议分析
这里，我们首先来分析一下上面代码的工作过程。 Prorif 从标有process 的主进程开始分析。现在我们来看看流程背后的内容。
首先，为客户端A生成非对称加密私钥skA，为服务器B生成签名私钥skB，生成相应的公钥（pkA，pkB），并将公钥发送出去。公共通道c. 发送这两个公钥。
接下来调用两个进程宏clientA和serverB，实现两个进程同时执行。在这里，我们使用复制来允许两个主题在无限会话中同时运行（clientA 和serverB 之前的感叹号表示这一点）。同时重复无限次会话）。
接下来重点关注两个模块：clientA 和serverB。首先，A 发送其公钥pkA 并创建对称密钥k（此处k 充当临时会话）。钥匙）。
然后B将临时密钥k和他的公钥pkB打包成一个元组，首先用他的私钥skB（签名部分）对其进行签名，然后用收到的公钥pkX对其进行加密，并通过公共通道发送（Send）。 aenc 部分（aenc 代表非对称加密）。
A接收通过通道发送的比特串，用自己的私钥解密，解密成功后获得y，并使用B的公钥pkB验证签名。元组（m，k）。第一项是pkB（这里我们用=pkB来匹配），第二项是对称密钥。 kA利用这个k对消息s进行对称加密，并在B收到传输的比特串后发送出去。使用您刚刚创建的对称密钥。用密钥k 解密产生内容z。这必须与s 具有相同的内容。
可以看到这段代码非常简单，所以不难想到中间人攻击。
proverif协议分析
将上述代码保存为ex_handshake.pv 文件，并运行以下命令来获取provif对上述握手协议的分析。
证明ex_handshake.pv
ProVerif 输出其考虑的流程的内部表示，并一次处理逻辑中的查询（由查询关键字表示）。查询攻击者的输出可以分为：个部分。
详细缩写： 通过proverif推断出导致被追踪的详细攻击的过程： 解释上述攻击结果的轨迹： 最终结论，true表示没有攻击，false表示攻击者没有相关信息，表示您正在获取
让我们从缩写部分开始逐部分地看。
攻击者使用已知的私钥k_3生成对应的公钥pk(k_3)（对应缩写的前两步，其中k_3要么是攻击者自己生成的，要么是通过其他方式获知的）。
那么这里标记的是代码的{16}位置。这说明可以从通道中收到攻击者发送的公钥pk(k_3)，同时收到消息aenc(sign((spk(skB) [] ),k_2),skB[]),pk (k_3) ) 此时消息已通过通道发送。
攻击者可以收到此消息（即攻击者可以获得此信息）。
然后攻击者从通道中检索此加密消息（aenc）并使用私钥k_3对其进行解密以获得sign((spk(skB[],k_2),skB[]))，可以通过以下方式获得签名。通过getmess(即(spk(skB[]),k_2))内容。这意味着攻击者可以获得k_2。
然后攻击者获得A的公钥pkA并使用该公钥加密并发送sign((spk(skB[]),k_2),skB[])。
客户端在{10} 收到此消息。验证签名后，客户端在{13}处发送消息senc(s[],k_2)，攻击者收到该消息。
然后攻击者可以使用k_2解密并获得s[]。
接下来看一下详细的输出部分。
前两行对应于创建公钥对和签名密钥对的过程。然后有三个输出，前两个输出代表攻击者将加密公钥和签名公钥分别存储在~M和~M_1中，第三个输出代表攻击者将加密公钥和签名公钥分别存储在~M和~M_1中。分别为~M_1，第三个输出代表另存为： M_2。从开始，每个后续行后面都跟有in copy a 或in copy a_2。相同的标识符表示相同的会话。 copy a表示当前攻击者正在与客户端通信，copy a_2表示当前攻击者正在通信。这意味着攻击者向服务器发送公钥，服务器返回一条用服务器私钥签名和加密的消息。现在攻击者将此消息保存为~M_3。然后，此处的攻击者{10} 使用私钥a_1 解密~M_3，使用客户端的公钥（其中~M 是客户端的公钥）对其进行加密，并解密加密的方式来发送消息。当客户端返回{13}加密消息时，攻击者可以使用k_4解密并获取s。
接下来改进协议，在协议中添加认证验证。
(* 客户端认为它正在使用对称密钥与服务器通信*)
该事件接受Client(key)。
(* 服务器认为它正在使用由密钥对称密钥和pkey 公钥标识的客户端与协议进行交互*)
该事件接受Server(key,pkey)。
(*由pkey标识的客户端认为使用该密钥与服务器的协议交互完成*)
事件术语Client(key,pkey)。
(*服务端认为使用密钥对称密钥与客户端的协议交互结束*)
活动期间服务器（关键）。
（*对于每个最终使用对称密钥x 与服务器交互的客户端y，总有一个服务器将其标识为使用对称密钥x 与客户端y 交互*）
查询x:key，y:pkey；事件(termClient(x,y))==事件(acceptsServer(x,y))。
（* 最终与对称密钥x 交互的每个服务器始终具有与使用对称密钥x 与服务器交互的任何其他客户端不同的注入关系*）
查询x:key；inj-event(termServer(x))==inj-event(acceptsClient(x))。
完整协议如下：
(* 对称密钥加密*)
输入密码。
fun senc(bitstring, key): 位串；
减少所有m: 位串、k: 键。 sdec(senc(m,k),k)=m。
(*非对称密钥加密*)
类型滑雪。
输入“pkey”。
有趣的pk(skey): pkey。
有趣的aenc(bitstring, pkey): 位字符串。
减少所有m:位串，sk: skey。 adec(aenc(m,pk(sk)),sk)=m.
（*电子签名*）
输入“sskey”。
键入spkey。
有趣的spk(sskey): spkey。
有趣的符号（位串，sskey）:位串。
减少所有m: 位串，ssk: sskey getmess(sign(m,ssk))=m。
减少所有m:位串，ssk: sskey。 checksign(sign(m,ssk),spk(ssk))=m.
免费c:频道。
免费s:bitstring [私人]。
查询攻击者。
该事件接受Client(key)。
该事件接受Server(key,pkey)。
事件术语Client(key,pkey)。
活动期间服务器（关键）。
查询x:key，y:pkey；事件(termClient(x,y))==事件(acceptsServer(x,y))。
查询x:key；inj-event(termServer(x))==inj-event(acceptsClient(x))。
让clientA(pkA:pkey,skA:skey,pkB:spkey)=
输出（c，pkA）；
in(c,x: 位串);
设y=adec(x,skA)
让(=pkB,k:key)=checksign(y,pkB) in
(*客户端解密成功+验证成功后，假设允许使用密钥k进行通信*)
事件接受Client(k)；
输出（c，senc（s，k））；
(* 客户端正在工作，这次使用k 进行通信，其公钥为pkA *)
事件项Client(k,pkA)。
letserverB(pkB:spkey,skB:sskey,pkA:pkey)=
在（c，pkX:pkey）；
新k:key；
(* 服务器收到客户端的公钥pkX 并创建密钥k。这意味着服务器接受使用密钥k 与客户端pkX 进行通信*)
事件接受Server(k,pkX);
输出（c，aenc（符号（（pkB，k），skB），pkX））;
in(c,x: 位串);
设z=sdec(x,k)
(*如果收到的pkX确实是pkA，则认为服务器已经完成对称密钥k的执行*)
事件termServer(k) 如果pkX=pkA；
过程
新skA:skey；
新skB:sskey；
令pkA=pk(skA) in out(c,pkA);
pkB=spk(skB) in out(c,pkB);
( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB,pkA)) )
该版本仅增加了身份验证，但中间人攻击问题仍未解决。
第一个结果表明消息s 的安全性尚未满足。
第二个结果表明B（服务器）到A（客户端）的身份验证不充分。这意味着，如果客户端认为它已经完成了与服务器的协议过程，那么它实际上可能不是正在通信的服务器。客户端也使用协议，因为中介可以伪装成服务器并与客户端进行通信。
第三个结果表明A（客户端）到B（服务器）的认证是令人满意的。这意味着必须至少有一个客户端与自身进行协商，服务器才能认为它已经完成了协议过程。
因此，为了防止中间人攻击，应该改进该协议，将客户端的身份包含在服务器返回的信息中。
输入密码。
fun senc(bitstring, key): 位串；
减少所有m: 位串、k: 键。 sdec(senc(m,k),k)=m。
类型滑雪。
输入“pkey”。
有趣的pk(skey): pkey。
有趣的aenc(bitstring, pkey): 位字符串。
减少所有m:位串，sk: skey。 adec(aenc(m,pk(sk)),sk)=m.
输入“sskey”。
键入spkey。
有趣的spk(sskey): spkey。
有趣的符号（位串，sskey）:位串。
减少所有m: 位串，ssk: sskey getmess(sign(m,ssk))=m。
减少所有m:位串，ssk: sskey。 checksign(sign(m,ssk),spk(ssk))=m.
免费c:频道。
免费s:bitstring [私人]。
查询攻击者。
该事件接受Client(key)。
该事件接受Server(key,pkey)。
事件术语Client(key,pkey)。
活动期间服务器（关键）。
查询x:key，y:pkey；事件(termClient(x,y))==事件(acceptsServer(x,y))。
查询x:key；inj-event(termServer(x))==inj-event(acceptsClient(x))。
让clientA(pkA:pkey,skA:skey,pkB:spkey)=
输出（c，pkA）；
in(c,x: 位串);
设y=adec(x,skA)
（*检查此处以确认该包确实已提交给pkA*）
让(=pkA,=pkB,k:key)=checksign(y,pkB) in
事件接受Client(k)；
输出（c，senc（s，k））；
事件项Client(k,pkA)。
letserverB(pkB:spkey,skB:sskey,pkA:pkey)=
在（c，pkX:pkey）；
新k:key；
事件接受Server(k,pkX);
(* 在此输入客户端标识符pkX 进行通信*)
输出（c，aenc（符号（（pkX，pkB，k），skB），pkX））;
in(c,x: 位串);
设z=sdec(x,k)
事件termServer(k) 如果pkX=pkA；
过程
新skA:skey；
新skB:sskey；
令pkA=pk(skA) in out(c,pkA);
pkB=spk(skB) in out(c,pkB);
( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB,pkA)) )
现在您可以验证所有三个属性。
Needham-Schroeder Protocol
Needham-Schroeder 身份验证协议是一个多问题—— 响应协议，可以对抗重放攻击。每轮会话都会应用一个新的随机数。
A 向KDC 发送消息1，表明它想要与B 通信。 KDC 使用消息2 进行响应。 A指定的随机数R_A被添加到消息1中，并且R_A也包含在KDC的响应消息中。它的作用是确保消息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) in
out(c, aenc(NX, pkX));
if pkX = pkB then
event 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) in
event beginAparam(pkY);
new Nb: bitstring;
out(c, aenc((NY, Nb), pkY));
in(c, m3: bitstring);
if Nb = adec(m3, skB) then
if pkY = pkA then
event 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分析结果
这个查询表示当B的参数结束时，相应的B的参数开始是否受到注入攻击。由于结果是false，说明在这个情况下，检测到乐注入攻击。
这个查询表示当A的参数结束时，相应的A的参数开始是否受到注入攻击。由于结果是true，说明在这个情况下，没有检测到注入攻击。
这个查询表示攻击者是否能够获得A的某个密钥（可能是Na）。结果是true，说明攻击者无法获取此密钥
这个查询类似于上一个，表示攻击者是否能够获得A的另一个密钥。结果是true，说明攻击者无法获取此密钥。
这个查询表示攻击者是否能够获得B的某个密钥（可能是Na）。结果是false，说明攻击者能够获取此密钥。
这个查询类似于上一个，表示攻击者是否能够获得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) in
new Na: nonce;
out(c, aenc((Na, A), pkX)); (* msg 3 *)
in(c, m: bitstring); (* msg 6 *)
let (=Na, NX: nonce) = adec(m, skA) in
out(c, aenc(nonce_to_bitstring(NX), pkX)); (* msg 7 *)
if hostX = B then
event 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) in
event beginAparam(hostY);
out(c, (B, hostY)); (* msg 4 *)
in(c,ms: bitstring); (* msg 5 *)
let (pkY: pkey,=hostY) = checksign(ms, pkS) in
new Nb: nonce;
out(c, aenc((NY, Nb), pkY)); (* msg 6 *)
in(c, m3: bitstring); (* msg 7 *)
if nonce_to_bitstring(Nb) = adec(m3, skB) then
if hostY = A then
event 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) in
out(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 then
let skxA = if xA = A then skA else skB in
let 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) in
event beginBfull(xA, hostX, pkX, pkxA, Na, NX2);
(* Message 7 *)
out(c, encrypt(nonce_to_bitstring(NX2), pkX));
(* OK *)
if hostX = B || hostX = A then
event 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 then
let skxB = if xB = A then skA else skB in
let pkxB = pk(skxB) in
(* Real start of the role *)
(* Message 3 *)
in(c, m: bitstring);
let (NY: nonce, hostY: host) = decrypt(m, skxB) in
event 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 then
event 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) in
out(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分析结果
这个查询表示攻击者无法获取A的某些比特串（Na）。结果是true，表明系统在防止攻击者获取A的某些敏感比特串方面是成功的。
类似于前一个查询，这个查询表示攻击者无法获取A的另一组比特串（Nb）。结果是true，表明系统在保护A的敏感比特串上是成功的。
这个查询表示攻击者能够获取B的某些比特串（Na）。结果是false，这是一个潜在的漏洞，系统可能需要改进B的比特串保护措施，以防止攻击者获取关键信息
类似于前一个查询，这个查询表示攻击者能够获取B的另一组比特串（Nb）。结果是false，系统可能需要改进B的比特串保护机制
这个查询表示，在B参数结束时的注入事件不会导致在B参数开始时的注入事件。结果是true，表明系统在B参数的结束处成功防止了注入攻击。
类似于前一个查询，这个查询表示在B的完整数据结束时的注入事件不会导致在B的完整数据开始时的注入事件。结果是true，表明系统在B的完整数据结束处成功防止了注入攻击。
这个查询表示，在A参数结束时的注入事件会导致在A参数开始时的注入事件。这意味着系统在A参数的结束处未能防止注入攻击，结果是false，系统可能需要加强对A参数的注入攻击检测和防护措施。
类似于前一个查询，这个查询表示在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个月的网络安全初级计划，当你学完后，你基本可以从事一份网络安全相关的工作，比如渗透测试、Web渗透、安全服务、安全分析等岗位；其中，如果你等保模块学的好，还可以从事等保工程师。
综合薪资区间6k~15k
1、网络安全理论知识（2天）
①了解行业相关背景，前景，确定发展方向。
②学习网络安全相关法律法规。
③网络安全运营的概念。
④等保简介、等保规定、流程和规范。（非常重要）
2、渗透测试基础（1周）
①渗透测试的流程、分类、标准
②信息收集技术：主动/被动信息搜集、Nmap工具、Google Hacking
③漏洞扫描、漏洞利用、原理，利用方法、工具（MSF）、绕过IDS和反病毒侦察
④主机攻防演练：MS17-010、MS08-067、MS10-046、MS12-20等
3、操作系统基础（1周）
①Windows系统常见功能和命令
②Kali Linux系统常见功能和命令
③操作系统安全（系统入侵排查/系统加固基础）
4、计算机网络基础（1周）
①计算机网络基础、协议和架构
②网络通信原理、OSI模型、数据转发流程
③常见协议解析（HTTP、TCP/IP、ARP等）
④网络攻击技术与网络安全防御技术
⑤Web漏洞原理与防御：主动/被动攻击、DDOS攻击、CVE漏洞复现
5、数据库基础操作（2天）
①数据库基础
②SQL语言基础
③数据库安全加固
6、Web渗透（1周）
①HTML、CSS和JavaScript简介
②OWASP Top10
③Web漏洞扫描工具
④Web渗透工具：Nmap、BurpSuite、SQLMap、其他（菜刀、漏扫等）
那么，到此为止，已经耗时1个月左右。你已经成功成为了一名“脚本小子”。那么你还想接着往下探索吗？
阶段二：中级or高级网络安全工程师（看自己能力）
综合薪资区间15k~30k
7、脚本编程学习（4周）
在网络安全领域。是否具备编程能力是“脚本小子”和真正网络安全工程师的本质区别。在实际的渗透测试过程中，面对复杂多变的网络环境，当常用工具不能满足实际需求的时候，往往需要对现有工具进行扩展，或者编写符合我们要求的工具、自动化脚本，这个时候就需要具备一定的编程能力。在分秒必争的CTF竞赛中，想要高效地使用自制的脚本工具来实现各种目的，更是需要拥有编程能力。
零基础入门的同学，我建议选择脚本语言Python/PHP/Go/Java中的一种，对常用库进行编程学习
搭建开发环境和选择IDE，PHP环境推荐Wamp和XAMPP，IDE强烈推荐Sublime；
Python编程学习，学习内容包含：语法、正则、文件、 网络、多线程等常用库，推荐《Python核心编程》，没必要看完
用Python编写漏洞的exp,然后写一个简单的网络爬虫
PHP基本语法学习并书写一个简单的博客系统
熟悉MVC架构，并试着学习一个PHP框架或者Python框架 (可选)
了解Bootstrap的布局或者CSS。
阶段三：顶级网络安全工程师
如果你对网络安全入门感兴趣，那么你需要的话可以点击这里👉网络安全重磅福利：入门&进阶全套282G学习资源包免费分享！
学习资料分享
当然，只给予计划不给予学习资料的行为无异于耍流氓，这里给大家整理了一份【282G】的网络安全工程师从入门到精通的学习资料包，可点击下方二维码链接领取哦。
#以上关于密码协议形式化分析与可证明安全实验1——使用proverif来分析密码协议的相关内容来源网络仅供参考，相关信息请以官方公告为准！
原创文章，作者：CSDN，如若转载，请注明出处：https://www.sudun.com/ask/92697.html
