A formal analysis method for authentication protocols
Shudong Shi · Journal of Hubei Normal University · 2004
BAN(Burrows,Abadi and Needham)-like logic can aid the design,analysis,and verification of Authentication protocols used over open networks and distributed systems.This paper introduces BAN-like logic and then illustrates the limitations of BAN logic on protocol idealization as a survey of the current state of BAN-like logic.The conclusions are that BAN-like logic is still one of the main tools for analysis of authentication protocols,but protocol idealization is the fatal weakness of BAN-like logic.Suggestions are then made for future work.These conclusions will facilitate the development of formal methods for the analysis and design of authentication protocols.