可信计算平台匿名认证技术的设计和实现
|
摘要
Internet的开放性导致其在安全和可靠方面的缺陷,使得当前Internet的应用技术已经不能满足电子商务、电子政务等领域的安全需求,传统的信息防御措施不能有效的从源头解决网络信息安全问题。可信计算平台作为解决信息安全隐患的计算机软硬件实体,引起了人们越来越多的关注。可信匿名认证是可信计算平台的重要功能,旨在解决接入网络终端平台身份的真实性鉴别,匿名地保证了接入网络的终端设备都是可信的。TPM vl.2规范中的DAA方案着重于平台身份隐私的保护,却忽略了对平台基本配置信息的保护,不能有效地提供不同信任域之间的TPM身份认证,这使其很难适用于复杂的Internet环境中。
论文在深入研究了现有可信匿名认证方案的基础上,针对其不足之处,设计和实现一种高效安全的可信匿名认证协议,解决了分布式网络环境下平台的身份认证问题,主要的创新性工作有几下几点：
1)针对DAA方案中存在平台基本配置隐私泄露的缺陷,提出了一种基于代理的DAA认证机制。该方案在基于非对称双线对的DAA方案基础上,引入了验证代理完成对示证者的平台身份和完整性验证,有效地保护了平台配置信息的隐私,并且在LRSW假设和DBDH假设下满足不可伪造性、可控的匿名性等安全需求；
2)针对DAA方案仅提供单域认证的局限性,结合信任关系,提出了一种基于动态信任值的跨域认证机制,实现了不同信任域之间的TPM身份认证。该方案将信任关系量化为[0,1]之间的信任值,通过对域间信任值与信任阈值的比较动态地实现了TPM用户的跨域访问,有效地减小跨域认证时TPM的工作负载和DAA认证的时间开销；
3)论文利用TPM-Emulator,在Linux下搭建了可信计算平台环境,通过Glade编程开发了使用虚拟TPM芯片的图形软件,对提出的可信匿名认证方案进行了部分实现。
Because of the openness of Internet which leads to the defection of security and dependability, the current Internet application technology can't meet the security needs of application area such as electronic commerce affair and electronic government affair. The traditional information guard system can't solve the information security of the terminal effectively. Trusted Computing Platform is a computer with software and hardware entity to solve the problem of information security, which makes people pay more and more attention to it. Trusted anonymous authentication technology is a significant function of Trusted Computing Platform, accomplishing the identity authentication of terminal platform which accesses to the network, assuring that the terminal which accesses to the network is trusted anonymously. DAA scheme in TPM vl.2 specification focuses on the privacy of platform identity but the platform configuration information and can't support TPM identity authentication of different trust-domain effectively, which is not suitable for Internet.
By researching on some of the existing trusted anonymous authentication schemes, in allusion to the limitation of the schemes, a trusted anonymous authentication scheme with security and high-efficiency is designed and implemented in the thesis, which solves the problem of platform identity authentication in the distribute network environment. The main creative work is as follows:
1) In allusion to the disclosure of platform configuration information privacy, a DAA scheme based on agent is proposed. The scheme is based on the asymmetric pairing, which introduces an attestation agent instead of the verifier to verify the identity and integrity of the platform and protects the privacy of platform configuration information. The analysis shows that the scheme meets the need of unforgeability, user-controllable anonymity under LRSW assume and DBDH assume.
2) In allusion to the limitation of single domain authentication, by integrating trust-relation, a cross-domain authentication scheme based on trust value is proposed, which solves the TPM identity authentication in different trust-domain. The scheme quantizes trust relationship to trust value between 0 and 1, realizes cross-domain authentication by comparing trust value and expectation value, which can effectively diminish the workload of TPM and retrench the time expense on DAA authentication.
3) By using TPM-Emulator, the trusted computing platform environment is set up in Linux. The thesis develops software for using virtual TPM by Glade programming, and the proposed trusted anonymous attestation scheme is implemented partly.
论文在深入研究了现有可信匿名认证方案的基础上,针对其不足之处,设计和实现一种高效安全的可信匿名认证协议,解决了分布式网络环境下平台的身份认证问题,主要的创新性工作有几下几点：
1)针对DAA方案中存在平台基本配置隐私泄露的缺陷,提出了一种基于代理的DAA认证机制。该方案在基于非对称双线对的DAA方案基础上,引入了验证代理完成对示证者的平台身份和完整性验证,有效地保护了平台配置信息的隐私,并且在LRSW假设和DBDH假设下满足不可伪造性、可控的匿名性等安全需求；
2)针对DAA方案仅提供单域认证的局限性,结合信任关系,提出了一种基于动态信任值的跨域认证机制,实现了不同信任域之间的TPM身份认证。该方案将信任关系量化为[0,1]之间的信任值,通过对域间信任值与信任阈值的比较动态地实现了TPM用户的跨域访问,有效地减小跨域认证时TPM的工作负载和DAA认证的时间开销；
3)论文利用TPM-Emulator,在Linux下搭建了可信计算平台环境,通过Glade编程开发了使用虚拟TPM芯片的图形软件,对提出的可信匿名认证方案进行了部分实现。
Because of the openness of Internet which leads to the defection of security and dependability, the current Internet application technology can't meet the security needs of application area such as electronic commerce affair and electronic government affair. The traditional information guard system can't solve the information security of the terminal effectively. Trusted Computing Platform is a computer with software and hardware entity to solve the problem of information security, which makes people pay more and more attention to it. Trusted anonymous authentication technology is a significant function of Trusted Computing Platform, accomplishing the identity authentication of terminal platform which accesses to the network, assuring that the terminal which accesses to the network is trusted anonymously. DAA scheme in TPM vl.2 specification focuses on the privacy of platform identity but the platform configuration information and can't support TPM identity authentication of different trust-domain effectively, which is not suitable for Internet.
By researching on some of the existing trusted anonymous authentication schemes, in allusion to the limitation of the schemes, a trusted anonymous authentication scheme with security and high-efficiency is designed and implemented in the thesis, which solves the problem of platform identity authentication in the distribute network environment. The main creative work is as follows:
1) In allusion to the disclosure of platform configuration information privacy, a DAA scheme based on agent is proposed. The scheme is based on the asymmetric pairing, which introduces an attestation agent instead of the verifier to verify the identity and integrity of the platform and protects the privacy of platform configuration information. The analysis shows that the scheme meets the need of unforgeability, user-controllable anonymity under LRSW assume and DBDH assume.
2) In allusion to the limitation of single domain authentication, by integrating trust-relation, a cross-domain authentication scheme based on trust value is proposed, which solves the TPM identity authentication in different trust-domain. The scheme quantizes trust relationship to trust value between 0 and 1, realizes cross-domain authentication by comparing trust value and expectation value, which can effectively diminish the workload of TPM and retrench the time expense on DAA authentication.
3) By using TPM-Emulator, the trusted computing platform environment is set up in Linux. The thesis develops software for using virtual TPM by Glade programming, and the proposed trusted anonymous attestation scheme is implemented partly.
引文
[1]沈昌祥,张焕国,冯登国.信息安全综述[J].中国科学.2007,37(2)：129-150.
[2]林闯,彭雪海.可信网络研究[J].计算机学报.2005.5：751-758.
[3]Anderson J P. Computer Security Technology Planning Study, ESD-TR-73-51, ESD/AFSC, Hanscom AFB, Bedford, MA(Oct.1972) [NTIS AD-758 206]
[4]毛江华,胡英.可信计算：安全终结者[N].计算机世界报.2004：12-13.
[5]National Computer Security Center. NCSC-TG-005. Trusted Network Interpretation of the Trusted Computer System Evaluation Criteria[S]. USA: DOD,1987.7.
[6]Trusted Computing Group:TCG Specification Architecture Overview, Revision 1.2[EB/OL].2004.4. https://www.trustedcomputinggroup.org/
[7]Trusted Computing Group. PM Main Specification version 1.2[EB/OL].2003.10. https://www.trustedcomputinggroup.org/
[8]Trusted Computing Group. Trusted Computing Platform Alliance(TCPA) main specification version 1.1b[EB/OL].2002.2. https://www.trustedcomputing group.org/
[9]Trusted Computing Group. TPM specification version 1.2.Part1 Design Principe, Revision 1.3[EB/OL].2007.5. https://www.trustedcomputinggroup.org/
[10]马建峰,朱建明等.无线局域网安全—方法与技术[M].机械工业出版社.2005.
[11]Microsoft Security Model for the Next-Generation Secure Computing Base[EB/OL]. http//www.microsoft.com/resource/sngscb/documents ngscb security model. doe,2003.
[12]张新刚,梁慧军.可信计算的研究现状与展望[J].网络安全技术与应用.2007.1：58-60.
[13]阎希光,可信计算的研究及其发展[J].信息安全与通信保密.2006：18-20.
[14]Trusted Computing Group:TPM specification version 1.2.Part3 TPM Commands, Revision 103[EB/OL].2006.10. https://www.trustedcomputinggroup.org/
[15]TCG Software Stack(TSS) Specification Version 1.2 Level 1. Part1:Commands and Structures[EB/OL].2007.7. http://www.trustedcomputinggroup.org/
[16]秦戈,韩文报.关于可信计算平台模块的研究[J].信息工程大学学报.2006, (4)：341-344
[17]赵佳,沈昌祥.可信认证关键技术研究[D].北京：北京交通大学.2008.5.
[18]刘长军,唐朝京.RSA密码算法体制的研究及其实现[D].长沙：国防科技大学.2002.11.
[19]N. Koblitz, A. Menezes, S. Vanstone. The state of elliptic curve cryptography. Designs, Codes and Cryptography.2000,19.
[20]王洪涛,李大兴.基于椭圆曲线和双线性对的数字签名的研究[D].济南：山东大学.2006.11
[21]A. Kiayias, Y. Tsiounis, and M. Yung. Traceable signature[C].In Advances in Cryptology(EUROCRYPT 2004), volume 3027 of Lecture Notes in Computer Science, Springer-Verlag,2004:571-589.
[22]J. Camenisch and A. Lysyanskaya. A signature scheme with efficient protocols[C]. In S. Cimato, C. Galdi, and G. Persiano, editors, Security in Communication Networks. Third International Conference, SCN 2002, volume 2576 of LNCS, Springer Verlag,2003:268-289.
[23]J. Camenisch and M. Michels. A group signature scheme based on RSA-variants[R]. Technical Report RS, BRICS, University of Aarhus,1998:27.
[24]J. Camenisch, M. Sradler. Efficient group signature scheme for large group[C]. In Crypto'97, Springer-Verlag, LNCS 1294,1997:410-424.
[25]N. Baric and B. Pfitzmann. Collision-free accumulators and fail-stop signature scheme without trees[C]. In Advances in Cryptology-Eurocrypto,1997:480-494.
[26]G. Ateniese, J. Camenisch, M. Joye,and G. Tsudik. A practical and Provably secure coalition-resistant group signature scheme[C]. In Advances in Cryptology Crypto,2000:255-270.
[27]B. A. LaMacchia and A. M. Odlyzho. Computation of discrete logarithms in Prime Fields[J]. Designs, Code and Cryptography,1991.1(1):46-62.
[28]T. EIGamal. A sub-expontential logarithm for computing discrete logarithms over GF(P2)[J]. IEEE Trans on Information Theory,1985,31(4):473-481.
[29]Trusted Computing Group:TCG Specification Architecture Overview Revision 1.4 [EB/OL].2007.8. https://www.trustedcomputinggroup.org/
[30]TCG Trusted Network Connect. TNC Architecture for Interoperability Specification[EB/OL]. Version 1.0, Revision 4,2005.3, http:// www.trustedcomputinggroup.org/.
[31]Trusted Computing Group, TNC Federated Specification v1.0,2009.5
[32]Trusted Computing Group, TSM Specification v1.2,2006.1
[33]Trusted Computing Group, TNC IF-TNCCS Specification v1.2 2009.5
[34]Trusted Computing Group, TNC IF-T:Protocol Binding for Tunneled EAP Methods Specification v1.1,2007.5
[35]Trusted Computing Group, TNC IF-PEP:Protocol Bindings for RADIUS Specification v1.1,2007.2
[36]Trusted Computing Group, TNC IF-IMC Specification v1.2,2007.2
[37]Trusted Computing Group, TNC IF-IMV Specification v1.2,2007.2
[38]张新刚,刘妍.可信计算与可信网络.信息安全与通信保密[C].2006：85-87.
[39]Trusted Computing Group, TNC IF-MAP Binding for SOAP Specification v1.1, 2009.5
[40]Trusted Computing Group, TNC CESP Specification v1.0,2009.5
[41]J. Camenisch and A. Lysyanskaya. Efficient non-transferable anonymous multi-show credential system with optional anonymity revocation[C]. In B. Pfitzmann, editor, Advances in Cryptology-EUROCRYPT 2001, volume 2045 of LNCS, Springer Verlag,2001:93-118
[42]Brickell E, Camenisch J, Chen L. Direct anonymous attestation[C]. Proc. of the 11th ACM Conference on Computer and Communications Security. New York: ACM Press,2004:132-145.
[43]J.Camenisch and A. Lysyanskaya. Dynamic accumulators and application to efficient revocation of anonymous credentials[C]. In M. Yung, editor, Advances in Cryptology-CRYPTO 2002, volume 2442 of LNCS, springer Verlag, 2002:61-67
[44]郝黎明,陆松年.P2P信誉系统中基于可信计算技术的匿名机制研究[D].上海：上海交通大学.2008.6.
[45]He Ge. An Anonymous Authentication Scheme for Trusted Computing Platform[EB/OL]. http://eprint.iacr.org/2005/445.pdf,2005.11.
[46]He Ge. A Method to Implement Direct Anonymous Attestation[EB/OL]. http://citeseer.ist.psu.edu/ge06method.html,2006.11
[47]Haldar. Semantic Remote Attestation [D]. Irvine:University of Of California, 2006.
[48]Brickell E, L Chen,J Li. Simplified security notions of direct anonymous attestation and a concrete scheme from pairings[R].Cryptology ePrint Archive, Report 2008.10.
[49]Chen, Liqun; Morrissey, Paul. Pairing in Trusted Computing[C]. The-Second International Conference On Pairing Cryptography Proceedings,2008.9.
[50]Xiaofeng Chen, Dengguo Feng. A New Direct Anonymous Attestation Scheme from Bilinear Maps[C]. The 9th International Conference for Young Computer Scientist.2008:2308-2313
[51]Rudolph C. Covert identity information in direct anonymous attestation. In Venter, H., Eloff, M., Labuschagne, L., Eloff, J., von Solms, R., eds.:22nd IFIP TC-11 International Information Security Conference (SEC2007) on "New Approaches for Security, Privacy and Trust in Complex Environments"[C], Sandton, South Africa, May 14-16,2007. Proceedings. Volume 232 of IFIP International Federation for Information Processing. Springer, Boston (2007) 443-448。
[52]Ahmad-Reza Sadeghi, Christian Stuble. Property-based Attestation for Computing Platforms:Caring About Properties, Not Mechanisms[C]. Proceedings of New Security Paradigms Workshop 2004. New York:Association for Computing Machinery,2004:67-77.
[53]张志勇,裴庆祺.支持验证代理方的远征证明模型及其安全协议[J].西安电子科技大学学报.2009,36(1)：58-63.
[54]李听.对Diffie-Hellman协议的一种改进[J].计算机安全.2007,12：22-24.
[55]裴俐春,陈性元.一种基于信任度的跨异构域动态认证机制[J].计算机应用,2008,28(6)：1382-1384.
[56]樊蕊.跨域身份认证系统的研究和实现[D].西安电子科技大学.2007.
[57]黄辰林,王志英.动态信任关系建模和管理技术研究[D].长沙：国防科技大学.2005.9.
[58]张艳群,张辰.基于模糊理论的信任度评估模型[J].计算机工程与设计,2007,28(3).
[59]Wessels J. Applications of Ban-Logic. http://www.win.tue.nl/ipa/archive/springdays2001/banwessels.pdf,2001.4.
[60]Wenbo Mao, Colin Boyd. Towards Formal Analysis of Security Protocols. In Computer Security Foundations Workshop Ⅵ, IEEE Computer Society Press, 1998,4:147-158.
[2]林闯,彭雪海.可信网络研究[J].计算机学报.2005.5：751-758.
[3]Anderson J P. Computer Security Technology Planning Study, ESD-TR-73-51, ESD/AFSC, Hanscom AFB, Bedford, MA(Oct.1972) [NTIS AD-758 206]
[4]毛江华,胡英.可信计算：安全终结者[N].计算机世界报.2004：12-13.
[5]National Computer Security Center. NCSC-TG-005. Trusted Network Interpretation of the Trusted Computer System Evaluation Criteria[S]. USA: DOD,1987.7.
[6]Trusted Computing Group:TCG Specification Architecture Overview, Revision 1.2[EB/OL].2004.4. https://www.trustedcomputinggroup.org/
[7]Trusted Computing Group. PM Main Specification version 1.2[EB/OL].2003.10. https://www.trustedcomputinggroup.org/
[8]Trusted Computing Group. Trusted Computing Platform Alliance(TCPA) main specification version 1.1b[EB/OL].2002.2. https://www.trustedcomputing group.org/
[9]Trusted Computing Group. TPM specification version 1.2.Part1 Design Principe, Revision 1.3[EB/OL].2007.5. https://www.trustedcomputinggroup.org/
[10]马建峰,朱建明等.无线局域网安全—方法与技术[M].机械工业出版社.2005.
[11]Microsoft Security Model for the Next-Generation Secure Computing Base[EB/OL]. http//www.microsoft.com/resource/sngscb/documents ngscb security model. doe,2003.
[12]张新刚,梁慧军.可信计算的研究现状与展望[J].网络安全技术与应用.2007.1：58-60.
[13]阎希光,可信计算的研究及其发展[J].信息安全与通信保密.2006：18-20.
[14]Trusted Computing Group:TPM specification version 1.2.Part3 TPM Commands, Revision 103[EB/OL].2006.10. https://www.trustedcomputinggroup.org/
[15]TCG Software Stack(TSS) Specification Version 1.2 Level 1. Part1:Commands and Structures[EB/OL].2007.7. http://www.trustedcomputinggroup.org/
[16]秦戈,韩文报.关于可信计算平台模块的研究[J].信息工程大学学报.2006, (4)：341-344
[17]赵佳,沈昌祥.可信认证关键技术研究[D].北京：北京交通大学.2008.5.
[18]刘长军,唐朝京.RSA密码算法体制的研究及其实现[D].长沙：国防科技大学.2002.11.
[19]N. Koblitz, A. Menezes, S. Vanstone. The state of elliptic curve cryptography. Designs, Codes and Cryptography.2000,19.
[20]王洪涛,李大兴.基于椭圆曲线和双线性对的数字签名的研究[D].济南：山东大学.2006.11
[21]A. Kiayias, Y. Tsiounis, and M. Yung. Traceable signature[C].In Advances in Cryptology(EUROCRYPT 2004), volume 3027 of Lecture Notes in Computer Science, Springer-Verlag,2004:571-589.
[22]J. Camenisch and A. Lysyanskaya. A signature scheme with efficient protocols[C]. In S. Cimato, C. Galdi, and G. Persiano, editors, Security in Communication Networks. Third International Conference, SCN 2002, volume 2576 of LNCS, Springer Verlag,2003:268-289.
[23]J. Camenisch and M. Michels. A group signature scheme based on RSA-variants[R]. Technical Report RS, BRICS, University of Aarhus,1998:27.
[24]J. Camenisch, M. Sradler. Efficient group signature scheme for large group[C]. In Crypto'97, Springer-Verlag, LNCS 1294,1997:410-424.
[25]N. Baric and B. Pfitzmann. Collision-free accumulators and fail-stop signature scheme without trees[C]. In Advances in Cryptology-Eurocrypto,1997:480-494.
[26]G. Ateniese, J. Camenisch, M. Joye,and G. Tsudik. A practical and Provably secure coalition-resistant group signature scheme[C]. In Advances in Cryptology Crypto,2000:255-270.
[27]B. A. LaMacchia and A. M. Odlyzho. Computation of discrete logarithms in Prime Fields[J]. Designs, Code and Cryptography,1991.1(1):46-62.
[28]T. EIGamal. A sub-expontential logarithm for computing discrete logarithms over GF(P2)[J]. IEEE Trans on Information Theory,1985,31(4):473-481.
[29]Trusted Computing Group:TCG Specification Architecture Overview Revision 1.4 [EB/OL].2007.8. https://www.trustedcomputinggroup.org/
[30]TCG Trusted Network Connect. TNC Architecture for Interoperability Specification[EB/OL]. Version 1.0, Revision 4,2005.3, http:// www.trustedcomputinggroup.org/.
[31]Trusted Computing Group, TNC Federated Specification v1.0,2009.5
[32]Trusted Computing Group, TSM Specification v1.2,2006.1
[33]Trusted Computing Group, TNC IF-TNCCS Specification v1.2 2009.5
[34]Trusted Computing Group, TNC IF-T:Protocol Binding for Tunneled EAP Methods Specification v1.1,2007.5
[35]Trusted Computing Group, TNC IF-PEP:Protocol Bindings for RADIUS Specification v1.1,2007.2
[36]Trusted Computing Group, TNC IF-IMC Specification v1.2,2007.2
[37]Trusted Computing Group, TNC IF-IMV Specification v1.2,2007.2
[38]张新刚,刘妍.可信计算与可信网络.信息安全与通信保密[C].2006：85-87.
[39]Trusted Computing Group, TNC IF-MAP Binding for SOAP Specification v1.1, 2009.5
[40]Trusted Computing Group, TNC CESP Specification v1.0,2009.5
[41]J. Camenisch and A. Lysyanskaya. Efficient non-transferable anonymous multi-show credential system with optional anonymity revocation[C]. In B. Pfitzmann, editor, Advances in Cryptology-EUROCRYPT 2001, volume 2045 of LNCS, Springer Verlag,2001:93-118
[42]Brickell E, Camenisch J, Chen L. Direct anonymous attestation[C]. Proc. of the 11th ACM Conference on Computer and Communications Security. New York: ACM Press,2004:132-145.
[43]J.Camenisch and A. Lysyanskaya. Dynamic accumulators and application to efficient revocation of anonymous credentials[C]. In M. Yung, editor, Advances in Cryptology-CRYPTO 2002, volume 2442 of LNCS, springer Verlag, 2002:61-67
[44]郝黎明,陆松年.P2P信誉系统中基于可信计算技术的匿名机制研究[D].上海：上海交通大学.2008.6.
[45]He Ge. An Anonymous Authentication Scheme for Trusted Computing Platform[EB/OL]. http://eprint.iacr.org/2005/445.pdf,2005.11.
[46]He Ge. A Method to Implement Direct Anonymous Attestation[EB/OL]. http://citeseer.ist.psu.edu/ge06method.html,2006.11
[47]Haldar. Semantic Remote Attestation [D]. Irvine:University of Of California, 2006.
[48]Brickell E, L Chen,J Li. Simplified security notions of direct anonymous attestation and a concrete scheme from pairings[R].Cryptology ePrint Archive, Report 2008.10.
[49]Chen, Liqun; Morrissey, Paul. Pairing in Trusted Computing[C]. The-Second International Conference On Pairing Cryptography Proceedings,2008.9.
[50]Xiaofeng Chen, Dengguo Feng. A New Direct Anonymous Attestation Scheme from Bilinear Maps[C]. The 9th International Conference for Young Computer Scientist.2008:2308-2313
[51]Rudolph C. Covert identity information in direct anonymous attestation. In Venter, H., Eloff, M., Labuschagne, L., Eloff, J., von Solms, R., eds.:22nd IFIP TC-11 International Information Security Conference (SEC2007) on "New Approaches for Security, Privacy and Trust in Complex Environments"[C], Sandton, South Africa, May 14-16,2007. Proceedings. Volume 232 of IFIP International Federation for Information Processing. Springer, Boston (2007) 443-448。
[52]Ahmad-Reza Sadeghi, Christian Stuble. Property-based Attestation for Computing Platforms:Caring About Properties, Not Mechanisms[C]. Proceedings of New Security Paradigms Workshop 2004. New York:Association for Computing Machinery,2004:67-77.
[53]张志勇,裴庆祺.支持验证代理方的远征证明模型及其安全协议[J].西安电子科技大学学报.2009,36(1)：58-63.
[54]李听.对Diffie-Hellman协议的一种改进[J].计算机安全.2007,12：22-24.
[55]裴俐春,陈性元.一种基于信任度的跨异构域动态认证机制[J].计算机应用,2008,28(6)：1382-1384.
[56]樊蕊.跨域身份认证系统的研究和实现[D].西安电子科技大学.2007.
[57]黄辰林,王志英.动态信任关系建模和管理技术研究[D].长沙：国防科技大学.2005.9.
[58]张艳群,张辰.基于模糊理论的信任度评估模型[J].计算机工程与设计,2007,28(3).
[59]Wessels J. Applications of Ban-Logic. http://www.win.tue.nl/ipa/archive/springdays2001/banwessels.pdf,2001.4.
[60]Wenbo Mao, Colin Boyd. Towards Formal Analysis of Security Protocols. In Computer Security Foundations Workshop Ⅵ, IEEE Computer Society Press, 1998,4:147-158.