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
Logics of Knowledge and Cryptography: Completeness and Expressiveness
KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
2007 (English)Doctoral thesis, monograph (Other scientific)
Abstract [en]

An understanding of cryptographic protocols requires that we examine the knowledge of protocol participants and adversaries: When a participant receives a message, does she know who sent it? Does she know that the message is fresh, and not merely a replay of some old message? Does a network spy know who is talking to whom?

This thesis studies logics of knowledge and cryptography. Specifically, the thesis addresses the problem of how to make the concept of knowledge reflect feasible computability within a Kripke-style semantics. The main contributions are as follows.

1. A generalized Kripke semantics for first-order epistemic logic and cryptography, where the later is modeled using private constants and arbitrary cryptographic operations, as in the Applied Pi-calculus.

2. An axiomatization of first-order epistemic logic which is sound and complete relative to an underlying theory of cryptographic terms, and to an omega-rule for quantifiers. Besides standard axioms and rules from first-order epistemic logic, the axiomatization includes some novel axioms for the interaction between knowledge and cryptography.

3. Epistemic characterizations of static equivalence and Dolev-Yao message deduction.

4. A generalization of Kripke semantics for propositional epistemic logic and symmetric cryptography.

5. Decidability, soundness and completeness for propositional BAN-like logics with respect to message passing systems. Completeness and decidability are generalised to logics induced from an arbitrary base of protocol specific assumptions.

6. An epistemic definition of message deduction. The definition lies between weaker and stronger versions of Dolev-Yao deduction, and coincides with weaker Dolev-Yao regarding all atomic messages. For composite messages, the definition withstands a well-known counterexample to Dolev-Yao deduction.

7. Protocol examples using mixes, a Crowds style protocol, and electronic payments.

Place, publisher, year, edition, pages
Stockholm: KTH , 2007. , xiii, 134 p.
Series
Trita-CSC-A, ISSN 1653-5723
Keyword [en]
epistemic logic, first-order logic, formal cryptography, static equivalence, security protocols, BAN logic, multi-agent system, completeness, logical omniscience problem
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-4424ISBN: 978-91-7178-705-7 (print)OAI: oai:DiVA.org:kth-4424DiVA: diva2:12265
Public defence
2007-06-15, E2, main building, Lindstedtsvägen 3, KTH, 10:00 (English)
Opponent
Supervisors
Note
QC 20100524Available from: 2007-06-04 Created: 2007-06-04 Last updated: 2010-05-24Bibliographically approved

Open Access in DiVA

fulltext(898 kB)668 downloads
File information
File name FULLTEXT01.pdfFile size 898 kBChecksum MD5
4ca5037b335226f69c554e542a89d4f937284410b6a06abe7968d382776ad45257c9dd7f
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Cohen, Mika
By organisation
Numerical Analysis and Computer Science, NADA
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 668 downloads
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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 611 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