Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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, Published 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.
Series
IEEE Symposium on Logic in Computer Science, ISSN 1043-6871
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-40709DOI: 10.1109/LICS.2007.4ISI: 000248944000008Scopus ID: 2-s2.0-78650511607ISBN: 978-0-7695-2908-0 (print)OAI: oai:DiVA.org:kth-40709DiVA: diva2:442697
Conference
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

Authority records BETA

Dam, Mads

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 122 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf