Page 242 - 《软件学报》2021年第9期

2866 Journal of Software 软件学报 Vol.32, No.9, September 2021

[16] Bhargavan K, Blanchet B, Kobeissi N. Verified models and reference implementations for the TLS 1.3 standard candidate. In: Proc.
of the 2017 IEEE Symp. on Security and Privacy (SP). IEEE, 2017. 483−502.
[17] Krawczyk H, Wee H. The OPTLS protocol and TLS1.3. In: Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer
Society, 2016. 81−96.
[18] Somorovsky J. Systematic fuzzing and testing of TLS libraries. In: Proc. of the ACM Sigsac Conf. on Computer and
Communications Security. ACM, 2016. 1492−1504.
[19] Xue R, Feng DG. The approaches and technologies for formal verification of security protocols. Chinese Journal of Computers,
2006,29(1):1−20 (in Chinese with English abstract).
[20] Cremers C. Scyther: Semantics and verification of security protocols. Netherlands: Eindhoven University of Technology, 2006.
[21] Cremers C. Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2. In: Proc. of the European Symp. on Research in
Computer Security (ESORICS 2011). Berlin: Springer-Verlag, 2011. 315−334.
[22] Basin D, Cremers C, Meier S. Provably repairing the ISO/IEC 9798 standard for entity authentication. Journal of Computer
Security, 2013,21(6):817−846.
[23] Yang H, Prinz A, Oleshchuk V. Formal analysis and model checking of a group authentication protocol by Scyther. In: Proc. of the
Euromicro Int’l Conf. on Parallel, Distributed, and Network-based Processing. IEEE Computer Society, 2016. 553−557.
[24] Yang H, Oleshchuk V, Prinz A. Verifying group authentication protocols by scyther. Journal of Wireless Mobile Networks,
Ubiquitous Computing, and Dependable Applications (JoWUA), 2016,7(2):3−19.
[25] Ray B, Chowdhury M, Abawajy J. Secure object tracking protocol for the Internet of things. IEEE Internet of Things Journal, 2016,
3(4):1−10.
[26] Meier S, Cremers C, Basin D. Strong invariants for the efficient construction of machine-checked protocol security proofs. In: Proc.
of the IEEE Computer Security Foundations Symp. IEEE Computer Society, 2010. 231−245.
[27] Meier S, Schmidt B, Cremers C, et al. The TAMARIN prover for the symbolic analysis of security protocols. In: Proc. of the Int’l
Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2013. 696−701.
[28] Canetti R, Krawczyk H. Analysis of key-exchange protocols and their use for building secure channels. In: Proc. of the Advances in
Cryptology (EUROCRYPT 2001). Berlin: Springer-Verlag, 2001. 453−474.
[29] Günther C. An identity-based key-exchange protocol. In: Proc. of the Workshop on the Theory and Application of of Cryptographic
Techniques. Berlin: Springer-Verlag, 1989. 29−37.
[30] Cha J, Cheon J. An identity-based signature from gap diffie-hellman groups. In: Proc. of the Int’l Workshop on Theory and Practice
in Public Key Cryptography: Public Key Cryptography. Berlin: Springer-Verlag, 2002. 18−30.
[31] Fischlin M, Günther F. Multi-stage key exchange and the case of Google’s QUIC protocol. In: Proc. of the 2014 ACM SIGSAC
Conf. on Computer and Communications Security. ACM, 2014. 1193−1204.
[32] Cremers C. Formally and practically relating the CK, CK-HMQV, and eCK security models for authenticated key exchange.
Cryptology Eprint Archive, 2009.
[33] Cremers C. Examining indistinguishability-based security models for key exchange protocols: The case of CK, CK-HMQV, and
eCK. In: Proc. of the ACM Symp. on Information, Computer and Communications Security. ACM, 2011. 80−91.
[34] Gorantla M, Boyd C, Nieto J. Modeling key compromise impersonation attacks on group key exchange protocols. ACM Trans. on
Information & System Security, 2009,14(4):1−24.

附中文参考文献:
[19] 薛锐,冯登国.安全协议的形式化分析技术与方法.计算机学报,2006,29(1):1−20.

陆思奇(1990－),男,讲师,主要研究领域为 毛颖(1994－),女,博士生,主要研究领域为
密码学,信息安全,安全协议形式化分析. 密码学,信息安全,安全协议形式化分析.

周思渊(1990－),男,研究实习员,主要研究
领域为密码学,信息安全.