A Complete Axiomatization of Knowledge and Cryptography

The combination of first-order epistemic logic and formal cryptography offers a potentially very powerful framework for security protocol verification. In this article, we address two main challenges towards such a combination; First, the expressive power, specifically the epistemic modality, needs to receive concrete computational justification. Second, the logic must be shown to be, in some sense, formally tractable. Addressing the first challenge, we provide a generalized Kripke semantics that uses permutations on the underlying domain of cryptographic messages to reflect agents’ limited computational power. Using this approach, we obtain logical characterizations of important concepts of knowledge in the security protocol literature, namely Dolev-Yao style message deduction and static equivalence. Answering the second challenge, we exhibit an axiomatization which is sound and complete relative to the underlying theory of cryptographic terms, and to an omega rule for quanti...

• Type: Conference
• Year: 2007
• Where: LICS
• Authors: Mika Cohen, Mads Dam
• Keywords: Computer Science, LICS 2007, Security Protocol, Security Protocol Verification, first-order Epistemic Logic