A Review and Comparative Analysis of Modal Logics:BAN,GYN,and SVO
Tanuja Thakur · 2015
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.