Logical Omniscience in the Semantics of BAN Logics
Mika Cohen, Mads Dam · 2003
BAN logic is an epistemic logic for verification of cryptogra phic protocols. A number of semantics have been proposed for BAN logic, but none of them capture the intended meaning of the epistemic modality in a satisfactory way. This is due to the so-called logical omniscience problem : Agents are ”ideal reasoners” in existing semantics, while agents in BAN logic have only limited cryptographic reasoning powers. Logical omniscience is unavoidable in Kripke semantics, the standard semantical framework in epistemic logic. Our proposal is to generalize the epistemic accessibility rela tion of Kripke semantics so that it changes not only the current execution point, but also the currently predicated message. When instantiated on message passing systems, the semantics validates BAN logic. It makes agents introspective (”self-aware”) of their own knowledge and of their own actions of sending, receiving and extracting.