Change search
ReferencesLink to record
Permanent link

Direct link
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.
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
URN: urn:nbn:se:kth:diva-4424ISBN: 978-91-7178-705-7OAI: diva2:12265
Public defence
2007-06-15, E2, main building, Lindstedtsvägen 3, KTH, 10:00 (English)
QC 20100524Available from: 2007-06-04 Created: 2007-06-04 Last updated: 2010-05-24Bibliographically approved

Open Access in DiVA

fulltext(898 kB)611 downloads
File information
File name FULLTEXT01.pdfFile size 898 kBChecksum MD5
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: 611 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

Total: 578 hits
ReferencesLink to record
Permanent link

Direct link