Change search
ReferencesLink to record
Permanent link

Direct link
A complete axiomatization of knowledge and cryptography
KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2007 (English)In: 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings, 2007, 77-86 p.Conference paper (Refereed)
Abstract [en]

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
National Category
Computer and Information Science
URN: urn:nbn:se:kth:diva-40709DOI: 10.1109/LICS.2007.4ISI: 000248944000008ScopusID: 2-s2.0-78650511607ISBN: 978-0-7695-2908-0OAI: diva2:442697
22nd Annual IEEE Symposium on Logic in Computer Science Location: Wroclaw, Poland, Date: JUL 10-14, 2007
Available from: 2011-09-22 Created: 2011-09-20 Last updated: 2012-01-20Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Cohen, MikaDam, Mads
By organisation
Numerical Analysis and Computer Science, NADATheoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 108 hits
ReferencesLink to record
Permanent link

Direct link