A Review and Comparative Analysis of Modal Logics:BAN,GYN,and SVO

  • Tanuja Thakur Kangra, H.P

Abstract

Traditionally, security protocols have been designed and verified using various techniques. Formal logics have been used to identify a number of flaws in protocolspreviously considered to be secure. The selection of proper modal logic is a crucial goal in the protocol analysis and verification process. This paper gives a comparative study of modal logics, which are widely used in modeling of security protocols. We will focus on logics of authentication.However, we will not only be discussing logics,but also be looking at the ‘rhyme and reason’ of authentication, the attempts to formalize and define notions of authentication and to apply these. Thus, we will also be considering the logic of authentication in a broader sense. This paper discusses three modal logics: BAN, SVO, and GYN. A formal analysis of these three has been presented.

Downloads

Download data is not yet available.

References

[1] John T. Kohl, B. Clifford Neuman, and Theodore Y. T'so, The Evolution of the Kerberos Authentication System. In Distributed Open Systems, pages 78-94. IEEE Computer Society Press, 1994.
[2] Tom Yu, Sam Hartman, and Ken Raeburn. The Perils of Unauthenticated Encryption: Kerberos Version 4. In Proceedings of the Network and Distributed System Security Symposium. The Internet Society, February 2004.
[3] B. Clifford Neuman and Theodore Ts'o. Kerberos: An Authentication Service for Computer Networks, IEEE Communications, 32(9):33-38. September 1994.
[4] Abdelmajid, N.T., Hossain M.A., Shepherd, S., Mahmoud, K (2010), “Improved Kerberos Security Protocol Evaluation using Modified BAN Logic”, IEEE Computer and Information Technology (CIT).
[5] Bellovin S. M., M. Merritt, “Limitations of the Kerberos Authentication System” Computer Communication Review, 20, pp 119-132, 1991.
[6] Clark John and Jeremy Jacob, “A survey of authentication protocol literature”, 1997.
[4] Bhandari R., S. Sharma, and N. Sharma, “Analysis of Windows Authentication Protocols: NTLM and Kerberos,” in International Conf. on Computer Networks and Information Technology. Chandigarh, pp. 254-263, 2014.
[7] Neuman C., T. Yu, S. Hartman, K. Raeburn, “The Kerberos Network Authentication System” (RFC4120) July 2005.
[8] Yu Tom, Sam Hartman, and Ken Raeburn, "The Perils of Unauthenticated Encryption: Kerberos Version 4”. In Proceedings of the Network and Distributed System Security Symposium. The Internet Society, February 2004.
[9] http://web.mit.edu/kerberos/papers.html
[10] http://kerberos.org/software/tutorial.html.
Published
2015-04-30
How to Cite
THAKUR, Tanuja. A Review and Comparative Analysis of Modal Logics:BAN,GYN,and SVO. International Journal of Research and Engineering, [S.l.], v. 2, n. 4, p. 30-33, apr. 2015. ISSN 2348-7860. Available at: <https://digital.ijre.org/index.php/int_j_res_eng/article/view/58>. Date accessed: 15 sep. 2019.

Keywords

Authentication, authentication protocol, modal logic, BAN, SVO, GYN