  While there have been many attempts, going back to BAN logic, to base
reasoning about security protocols on epistemic notions, they have not been all
that successful. Arguably, this has been due to the particular logics chosen.
We present a simple logic based on the well-understood modal operators of
knowledge, time, and probability, and show that it is able to handle issues
that have often been swept under the rug by other approaches, while being
flexible enough to capture all the higher- level security notions that appear
in BAN logic. Moreover, while still assuming that the knowledge operator allows
for unbounded computation, it can handle the fact that a computationally
bounded agent cannot decrypt messages in a natural way, by distinguishing
strings and message terms. We demonstrate that our logic can capture BAN logic
notions by providing a translation of the BAN operators into our logic,
capturing belief by a form of probabilistic knowledge.
