Logical Omniscience in the Semantics of BAN Logics
2005 (English)Conference paper (Refereed)
BAN logic is an epistemic logic for verification of cryptographic 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 relation of Kripke semantics so that it changes not only the current execution point, but also the currently predicated message. When nstantiated 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.
Place, publisher, year, edition, pages
2005. 121-132 p.
BAN logic; Epistemic logic; Kripke semantics; Security protocols; Logical omniscience problem
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-62963OAI: oai:DiVA.org:kth-62963DiVA: diva2:481440