Page 19 - 《软件学报》2021年第6期

张协力 等:C2P:基于 Pi 演算的协议 C 代码形式化抽象方法和工具 1593

Fig.7 Case of call abstract
图 7 函数调用抽象逻辑正确性案例

这里采用 ProVerif 工具自动化证明命题 4.1 和命题 4.2,如图 8 所示.

Fig.8 Proof of correctness
图 8 正确性证明结果

由 ProVerif 对命题 4.1 和命题 4.2 的证明结果可知,两个命题均成立.事实上,借助 ProVerif 工具可以进一步
证明:在多个函数调用存在情况下,命题依然成立.据此,本文关于函数调用关系抽象的正确性得到证明,即根据
此方法得到的 Pi 演算抽象模型在执行逻辑上与协议 C 代码时一致的.

4.3 Kerberos协议代码分析
本节以一份 Kerberos 协议的示例代码作为分析对象,进一步说明本文方案对协议代码验证的有效性.该分
析对象为 github 上下载的一份 Kerberos 协议的 Demo 代码.该份代码实现的协议流程如下.
(1) A→B:A,B,N1;
(2) S→A:IV2,E(N1,B,Kab,IV_ticket,ticket) Ka,IV2 ;
(3) A→B:A,B,IV_ticket,ticket,IV3,E(N2) Kab,IV3 ;
(4) B→A:IV4,E(N2,N3) Kab,IV4 ;
(5) A→B:IV5,E(N2,N3) Kab,IV5 ;
(6) B→A:IV6,E(data) Kab,IV6 ;
(7) A→B:IV7,E(data*) Kab,IV7 .
其中,ticket=E(timestamp,A,Kab) Kb ,Ka 和 Kb 分别为实体 A,B 与可信第三方 S 共享的密钥,E 为对称加密算法, IV
为加密算法中用的初始向量.协议主要通信目标为实体 A 通过可信第三方 S 授权访问 B 上的资源 data.