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

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

[8] Chaki S, Datta A. ASPIER: An automated framework for verifying security protocol implementations. In: Proc. of the 22nd IEEE
Computer Security Foundations Symp. New York: IEEE, 2009. 172−185. [doi: 10.1109/CSF.2009.20]
[9] Aizatulin M, Gordon AD, Jürjens J. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In:
Chen Y, ed. Proc. of the 18th ACM Conf. on Computer and Communications Security. New York: ACM, 2011. 331−340. [doi:
10.1145/2046707.2046745]
[10] Aizatulin M, Gordon AD, Jürjens J. Computational verification of C protocol implementations by symbolic execution. In: Yu T, ed.
Proc. of the 2012 ACM Conf. on Computer and Communications Security. New York: ACM, 2012. 712−723. [doi: 10.1145/
2382196.2382271]
[11] Blanchet B. Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Foundations and Trends® in
Privacy and Security, 2016,1(1-2):1−135.
[12] Milner R. Communicating and Mobile Systems: The Pi Calculus. London: Cambridge University Press, 1999.
[13] Kiyomoto S, Ota H, Tanaka T. A security protocol compiler generating C source codes. In: Proc. of the 2008 Int’l Conf. on
Information Security and Assurance (ISA 2008). Piscataway: IEEE, 2008. 20−25.
[14] Backes M, Maffei M, Unruh D. Computationally sound verification of source code. In: Al-Shaer E, ed. Proc. of the 17th ACM Conf.
on Computer and Communications Security. New York: ACM, 2010. 387−398. [doi: 10.1145/1866307.1866351]
[15] Jürjens J. Automated security verification for crypto protocol implementations: Verifying the Jessie project. Electronic Notes in
Theoretical Computer Science, 2009,250(1):123−136. [doi: 10.1016/j.entcs.2009.08.009]
[16] Bhargavan K, Fournet C, Gordon AD, Tse S. Verified interoperable implementations of security protocols. ACM Trans. on
Programming Languages and Systems (TOPLAS), 2008,31(1):1−61. [doi: 10.1145/1452044.1452049]
[17] Tang WS, Gou ZL, Ahmadon MAB, Yamaguchi S. On verification of implementation of security specification with Petri nets’
protocol inheritance. In: Proc. of the IEEE 5th Global Conf. on Consumer Electronics. Piscataway: IEEE, 2016. 1−4. [doi: 10.1109/
GCCE.2016.7800491]
[18] Ahmadon MAB, Yamaguchi S, Gupta BB. Petri net-based verification of security protocol implementation in software evolution.
Int’l Journal of Embedded Systems, 2018,10(6):503−517. [doi: 10.1504/IJES.2016.10011276]
附中文参考文献:
[3] 孟博,鲁金钿,王德军,何旭东.安全协议实施安全性分析综述.山东大学学报(理学版),2018,53(1):1−18. [doi: 10.6040/j.issn.1671-
9352.2.2017.067]
[4] 张焕国,吴福生,王后珍,王张宜.密码协议代码执行的安全验证分析综述.计算机学报,2018,41(2):288−308. [doi: 10.11897/SP.J.
1016.2018.00288]

张协力(1992－),男,硕士,主要研究领域为 顾纯祥(1976－),男,博士,教授,博士生导
网络安全协议. 师,主要研究领域为网络安全,密码学.

祝跃飞(1962－),男,博士,教授,博士生导 陈熹(1988－),男,硕士,讲师,主要研究领
师,主要研究领域为网络安全,密码学. 域为网络空间安全,密码学,计算机网络.