Formal logics of knowledge have been employed for the verification of cryptographic protocols. Intuitively, the idea is that a correct run of a protocol should lead the participating agents to "know" some facts, due to the structure of the protocol. While there has been a great deal of work in this area, fundamental questions remain regarding the foundations of the approach. In fact, it is not even clear if any intrinsic properties of knowledge are actually required; in most cases the relevant notion of knowledge reduces directly to universal quantification over protocol runs. Moreover, there is no consensus about the appropriate epistemic domain for protocol participants, the nature of epistemic change, or the significance of initial knowledge. In this paper, we address these fundamental questions by revisiting the epistemic foundations of protocol verification.
展开▼
