密码协议形式化分析与可证明安全实验一——ProVerif实验

安装ProVerif

环境：win10 x64

Windows 用户使用二进制发行版安装 ProVerif。选择任意一个地址创建ProVerif文件夹。后续所有安装程序压缩包均解压至该文件夹下。

在此，本作者选择在D盘创建ProVerif文件夹，即D:\ProVerif

安装 graphviz

Graphviz 可以从 官网 下载： graphviz-9.0.0 (64位) EXE安装程序[sha256]。解压至D:\ProVerif

环境变量配置如下所示：

右击“此电脑”->属性->高级系统设置->环境变量->系统变量->PATH

配置环境变量，确保添加bin文件的路径在系统PATH中。

安装GTK+2.24（选）

如果要运行交互式模拟器 proverif interact，则需要安装 GTK 2.24。

从官网下载版本：gtk+-bundle_2.24.10-20120208_win32.zip。 解压至D:\ProVerif

配置环境变量。

将bin文件添加至PATH中。

下载二进制版本ProVerif

在 网页中下载 ProVerif version 2.05, for Windows 和 ProVerif version 2.05, documention

下载完之后的压缩吧分别为: proverifbin2.05.tar.gz 和 proverifdoc2.05.tar.gz

将以上两个压缩吧解压到文件夹：D:\ProVerif 。

ProVerif 现已成功安装在解压文件的目录中。

我们按住win + r 打开后台，进入EXE应用程序所在目录：D:\ProVerif\proverifbin2.05\proverif2.05

查看proverif -help 帮助文档。这里用 -help 参数可以看到proverif是可用的

运行hello.pv文件

在D:\ProVerif\proverifbin2.05\proverif2.05 （exe应用程序所在目录）目录下新建txt文档，写入以下代码。

(* h e l l o . pv : H e l l o World S c r i p t *)

free c : channel .

free Cocks : bitstring [ private ] .
free RSA: bitstring [ private ] .

query attacker (RSA ) .
query attacker ( Cocks ) .

process
out ( c ,RSA ) ;
0

保存txt文档后修改文件名为hello.pv 。（很重要，一个文件只有文件名正确才能正确运行）

在终端运行该文件。

HandShake Protocol （握手协议 ）

代码

(* Symmetric Enc *)
type key.
fun senc(bitstring,key) : bitstring.
reduc forall m:bitstring,k:key;sdec(senc(m,k),k) = m.
(* Asymmetric Enc Structure *)
type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring,pkey): bitstring.
reduc forall m:bitstring,k:skey;adec(aenc(m,pk(k)),k) = m.
(* Digital Signatures Structure *)
type sskey.
type spkey.
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.
(* HandShake Protocol *)
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) in
let (=pkB,k:key) = checksign(y,pkB) in
out(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) in
0.
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)) )

协议分析

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

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

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

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

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

A通过信道接收到这个发来的bitstring（Line 46），然后用自己私钥解密，解密成功之后得到y（Line 47），之后用B的公钥pkB验证签名，如果验证通过了就会得到元组(m,k)，第一项就是pkB（Line 48， 这里用=pkB来匹配），第二项就是对称密钥k

A再用这个k给消息s进行对称加密然后发出去（Line 49），B接收到发来的bitstring之后，用自己刚刚创 建的对称密钥k解密就得到了内容z，这应该和s是一样的内容

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

proverif分析协议

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

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

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

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[] 

        1. 前两行对应的是公钥密钥对和签名密钥对的创建过程 

        2.然后是三个out，前两个out表示attacker将加密公钥和签名公钥分别保存在 ~M 和 ~M_1         中，第三个out表示client在{9}处的输出，attacker将其保存为 ~M_2

        3.从Line 9开始，之后的每一行后面都跟了一个 in copy a 或者 in copy a_2 ，相同的标识表示相同的会话， copy a 表示当前attacker正在与client进行通信， copy a_2 表示当前attacker正在和 server通信

        4.这里看Line 11-15，表示attacker向server发送了一个公钥，同时server返回了一个用server私钥签名并加密的消息，这里attacker将这条消息保存为 ~M_3 （Line 15）

        5.然后在看Line 17-19，这里表示attacker在{10}这里，用 a_1 这个私钥解密 ~M_3 ，再用client的公钥加密（这里的 ~M 就是client的公钥），将加密后的消息发送出去，当client在{13}返回加密的消息时，attacker可以利用 k_4 解密并获得 s 

这里可以回顾中间人攻击的流程，攻击者需要同时维护两个会话（对应于上面的两个会话），将从与 server会话接收到的内容选择性的篡改（也可以不改，上面的协议需要解密，所以修改了），然后发送 到与client的会话中

由于没有额外的方式完成鉴权（上述过程只有一个server的签名和认证），所以client和server都认为它们与对方建立了加密会话，而实际上这个加密会话所使用的密钥已经被attacker获取到了

协议改进

要解决中间人攻击，可以采用公钥基础设施（Public Key Infrastructure，PKI）来确保通信双方的公钥的真实性。PKI 包括证书颁发机构（Certificate Authority，CA）和数字证书，以确保公钥的合法性和身份验证。

数据类型和函数定义

• certificate: 表示数字证书的数据类型。
• CAkey: 表示证书颁发机构的公钥的数据类型。

type certificate.
type CAkey.

• issueCert(pkey): certificate: 用于颁发证书的函数，输入为公钥 pkey，输出为数字证书。
• verifyCert(certificate, CAkey): bool: 用于验证证书真实性的函数，输入为数字证书和证书颁发机构的公钥，输出为布尔值。

fun issueCert(pkey): certificate.
fun verifyCert(certificate, CAkey): bool.

 客户端 (clientA) 的协议部分

• 客户端生成自己的公钥 pkA 和私钥 skA，并向证书颁发机构请求证书 (certA)。
• 将自己的证书发送给服务器。
• 从服务器接收证书，并使用证书颁发机构的公钥 CAkeyA 来验证服务器的证书真实性。
• 如果验证通过，生成一对会话密钥 k，将公钥 pkB 和密钥 k 使用服务器的公钥 pkX 进行签名，并将签名后的数据发送给服务器。
• 接收服务器使用会话密钥加密的数据，并进行解密。

let clientA(pkA:pkey, skA:skey, CAkeyA:CAkey) =
    let certA = issueCert(pkA) in
    out(c, certA);  (* Send certificate to serverB *)
    
    in(c, x:certificate);  (* Receive serverB's certificate *)
    
    if verifyCert(x, CAkeyA) then
        let y = adec(x, skA) in
        let (=pkB, k:key) = checksign(y, spkA) in
        out(c, senc(s, k))
    else
        (* Certificate verification failed, abort the protocol *)
        out(c, abort);

服务器 (serverB) 的协议部分

• 服务器生成自己的公钥 pkB 和私钥 skB，并向证书颁发机构请求证书 (certB)。
• 接收客户端发送的证书，并使用证书颁发机构的公钥 CAkeyB 来验证客户端的证书真实性。
• 如果验证通过，生成一对会话密钥 k，将公钥 pkB 和密钥 k 使用客户端的公钥 pkX 进行签名，并将签名后的数据发送给客户端。
• 接收客户端使用会话密钥加密的数据。

let serverB(CAkeyB:CAkey, skB:sskey) =
    in(c, x:certificate);  (* Receive clientA's certificate *)
    
    let certB = issueCert(pkB) in
    out(c, certB);  (* Send serverB's certificate to clientA *)
    
    if verifyCert(x, CAkeyB) then
        new k:key;
        out(c, aenc(sign((pkB, k), skB), pkX));
        
        in(c, x:bitstring);
        let z = sdec(x, k) in
        0
    else
        (* Certificate verification failed, abort the protocol *)
        out(c, abort);

主进程

• 主进程生成客户端和服务器的公钥、私钥以及证书颁发机构的公钥。
• 启动客户端和服务器的进程，开始协议。

process
    new skA:skey;
    new skB:sskey;
    new CAkeyA:CAkey;
    new CAkeyB:CAkey;
    
    let pkA = pk(skA) in
    let spkA = spk(skA) in
    let pkB = spk(skB) in
    
    (!clientA(pkA, skA, CAkeyA) | !serverB(CAkeyB, skB))

在这个改进后的协议中，引入了证书的概念，并由证书颁发机构（CA）负责颁发和验证证书。issueCert 函数用于颁发证书，verifyCert 函数用于验证证书的真实性。

在握手协议的开始，clientA 和 serverB 交换各自的证书，并使用 CA 的公钥来验证对方的证书。只有在证书验证通过后，才继续执行协议。这样可以确保双方公钥的真实性，防止中间人攻击。

Needham-Schroeder Protocol

协议的主要目标是确保两个实体能够在通信中验证对方的身份，从而建立安全的通信渠道。这个协议通常用于解决"中间人攻击"（Man-in-the-Middle Attack）的问题，其中攻击者试图在通信实体之间插入自己，窃取或篡改通信内容。

本协议类似kerberos协议，有票据ticket的应用。在本协议中E_K_B[K_S||ID_A]就是用户A和用户B建立联系的票据。

协议过程 

如上图所示。

参数说明

• KDC是密钥分发中心
• ID是身份标识
• K_A,K_B分别是用户A，B和KDC的共享密钥
• N_1和N_2是两个随机数

过程 

1. A用户生成一个随机数N_1,将用户A和B的ID一起发送给KDC
2. KDC产生一个随机密钥K_S。KDC使用和用户B的共享密钥K_B加密随机密钥K_S和用户A的身份标识。KDC使用和用户A的共享密钥K_A 加密 随机密钥K_S和用户B的身份标识，随机数N_1和上一个加密结果。将结果发送给用户A。
3. 用户A使用共享密钥K_A解密。获得随机密钥K_S。获得用户B的身份标识，在此验证用户B是否就使通信对方。获得随机数N_1，用于验证KDC。获的E_K_B[K_S||ID_A]。用户A无脑发送给用户B解密获得的最后一部分内容：E_K_B[K_S||ID_A]
4. 用户B接受并解密。获得随机密钥K_S。获得用户A的身份标识，将此身份标识与发送方A的身份标识进行对比，验证发送方的身份。用户B生成一个随机数N_2，使用随机密钥K_S加密此随机数。发送给用户A。
5. 用户A使用K_S解密获得随机数N_2，作用函数后使用K_S加密发送给B

协议的目的是由KDC为A、B安全地分配会话密钥KS， A在第1步安全地获得了K_S，而第3步的消息仅能被B 解读，因此B在第3步安全地获得了KS，第4步中B向 A示意自己已掌握K_S，N_2用于向A询问自己在第3步收 到的K_S是否为一新会话密钥，第5步A对B的询问作出 应答，一方面表示自己已掌握K_S，另一方面由f(N_2 )回答了K_S的新鲜性 。可见第4、5两步用于防止一种类型的重放攻击，比如敌手在前一次执行协议时截获第3步的消息，然后在这次执行协议时重放，如果这 时没有第4、5两步的握手过程的话，B就无法检查出自己得到的K_S是重放的旧密钥 。

协议分析  

变体1

文件：NeedhamSchroederPK-var1.pv

运行结果

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

Query inj-event(endBparam(x)) ==> inj-event(beginBparam(x)) is false.

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

 Query inj-event(endAparam(x)) ==> inj-event(beginAparam(x)) is true.

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

Query not attacker(secretANa[]) is true.

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

 Query not attacker(secretANb[]) is true

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

Query not attacker(secretBNa[]) is false.

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

 Query not attacker(secretBNb[]) is 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的某些密钥。这是系统的一个积极方面，但仍然需要确保所有关键密钥都得到足够的保护。

变体2

文件：NeedhamSchroederPK-var2.pv

运行结果

 漏洞分析

同变体1一样。

变体3

文件：NeedhamSchroederPK-var3.pv

运行结果

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

Query not attacker_bitstring(secretANa[]) is true

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

Query not attacker_bitstring(secretANb[]) is true.

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

Query not attacker_bitstring(secretBNa[]) is false.

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

Query not attacker_bitstring(secretBNb[]) is false.

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

Query inj-event(endBparam(x,y)) ==> inj-event(beginBparam(x,y)) is false

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

Query inj-event(endBfull(x1,x2,x3,x4,x5,x6)) ==> inj-event(beginBfull(x1,x2,x3,x4,x5,x6)) is false.

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

Query inj-event(endAparam(x,y)) ==> inj-event(beginAparam(x,y)) is true.

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

 Query inj-event(endAfull(x1,x2,x3,x4,x5,x6)) ==> inj-event(beginAfull(x1,x2,x3,x4,x5,x6)) is true

漏洞分析 

A参数注入漏洞

• 漏洞分析： 可能存在未经过充分验证和过滤的A参数输入，导致在A参数结束时的注入事件影响了A参数的开始。
• 攻击方法： 攻击者可能会尝试通过在A参数结束时注入恶意代码或数据，来影响A参数的开始，执行未授权的操作或者篡改系统状态。

B参数比特串保护不足

• 漏洞分析： 暗示攻击者能够获取B参数的某些比特串，可能意味着存在对B参数比特串的不充分保护。
• 攻击方法： 攻击者可能会尝试通过拦截或者篡改B参数的比特串，来绕过安全控制，获取敏感信息或者执行未授权的操作。

A完整数据注入漏洞

• 漏洞分析： 暗示在A的完整数据结束时的注入事件可能影响A的完整数据的开始，表明存在对A完整数据注入的不足防护。
• 攻击方法： 攻击者可能会试图通过在A完整数据结束时注入恶意数据，来影响A完整数据的开始，导致数据不一致或者执行不当操作。

B完整数据注入漏洞

• 漏洞分析： 表明在B的完整数据结束时的注入事件无法有效防止在B的完整数据开始时的注入事件，存在B完整数据注入漏洞。
• 攻击方法： 攻击者可能会尝试通过在B完整数据结束时注入恶意数据，来绕过防护，影响B完整数据的开始，导致数据不一致或者执行不当操作。

参考文献

 http://course.sdu.edu.cn/Download/20150422102132005.pdf

 Needham-Schroeder协议原理及实现(Java)_needham-schroeder的原理-CSDN博客

Needham-Schroeder协议原理及实现(Java) | 码农家园 (codenong.com) 

Needham – Schroeder协议 - 华文百科 (wikii.one) 

Needham-Schroeder协议 – 编码人生 (codelife.me) 文章来源地址https://www.toymoban.com/news/detail-790669.html

到了这里，关于密码协议形式化分析与可证明安全实验一——ProVerif实验的文章就介绍完了。如果您还想了解更多内容，请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章，希望大家以后多多支持TOY模板网！