An Improved Security Protocol Formal Analysis with BAN Logic

BAN logic can prove whether a protocol can reach expected target and find some flaws in the protocol. The paper analyzed constitute of BAN logic and analysis steps. On the basis of the above work, BAN logic was used to construct an ideal model of the improved NSSK protocol and the security of the NSSK protocol was analyzed with the initial hypothesis and the logic postulate. The paper also pointed out various kinds of demerit of BAN logic and discussed some possible improvement.