Specifically, BAN logic helps its users determine whether exchanged information is trustworthy, secured against eavesdropping, or both.
BAN logic starts with the assumption that all information exchanges happen on media vulnerable to tampering and public monitoring.
Some of these try to repair one weakness of BAN logic: the lack of a good semantics with a clear meaning in terms of knowledge and possible universes.
However, starting in the mid-1990s, crypto protocols were analyzed in operational models (assuming perfect cryptography) using model checkers, and numerous bugs were found in protocols that were "verified" with BAN logic and related formalisms.
[citation needed] In some cases a protocol was reasoned as secure by the BAN analysis but were in fact insecure.
[3] This has led to the abandonment of BAN-family logics in favor of proof methods based on standard invariance reasoning.
If the proof fails, the point of failure usually suggests an attack which compromises the protocol.
The goal is to have A reads the clock, obtaining the current time t, and sends the following message: That is, it sends its chosen session key and the current time to S, encrypted with its private authentication server key KAS.