Formal Analysis for Security of Otway-Rees Protocol 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 Otway-Rees protocol and the security of the 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.