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

1594 Journal of Software 软件学报 Vol.32, No.6, June 2021

代码抽象的部分结果如图 9 所示.

Fig.9 Partial results of code abstraction
图 9 代码转换部分结果

抽象完成后,通过人工添加协议安全属性及部分语法修正,利用 ProVerif 工具自动化验证结果,如图 10 所示.

Fig.10 An attack path of Kerberos code
图 10 Kerberos 代码认证性攻击路径