A Complete Axiomatization of Knowledge and Cryptography

14 years 14 days ago
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...
Mika Cohen, Mads Dam
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where LICS
Authors Mika Cohen, Mads Dam
Comments (0)