A complete axiomatization of knowledge and cryptography
2007 (English)In: 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings, 2007, 77-86 p.Conference paper (Refereed)
The combination offirst-order epistemic logic with formal cryptography offers a potentially powerful framework for security protocol verification. In this paper cryptography is modelled using private constants and one-way computable operations, as in the Applied Pi-calculus. To give the concept of knowledge a computational justification, we propose a generalized Kripke semantics that uses permutations on the underlying domain of cryptographic messages to reflect agents' limited resources. This interpretation links the logic tightly to static equivalence, another important concept of knowledge that has recently been examined in the security protocol literature, and for which there are strong computational soundness results. We exhibit an axiomatization which is sound and complete relative to the underlying theory of terms, and to an omega-rule for quantifiers. Besides standard axioms and rules, the axiomatization includes novel axioms for the interaction between knowledge and cryptography. As protocol examples we use mixes, a Crowds-style protocol, and electronic payments. Funher more, we provide embedding results for BAN and SVO.
Place, publisher, year, edition, pages
2007. 77-86 p.
, IEEE Symposium on Logic in Computer Science, ISSN 1043-6871
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-40709DOI: 10.1109/LICS.2007.4ISI: 000248944000008ScopusID: 2-s2.0-78650511607ISBN: 978-0-7695-2908-0OAI: oai:DiVA.org:kth-40709DiVA: diva2:442697
22nd Annual IEEE Symposium on Logic in Computer Science Location: Wroclaw, Poland, Date: JUL 10-14, 2007