| 1. |
- Cohen, Mika, et al.
(författare)
-
A complete axiomatization of knowledge and cryptography
- 2007
-
Ingår i: 22nd Annual IEEE Symposium On Logic In Computer Science, Proceedings. - 9780769529080 ; , s. 77-86
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 2. |
- Cohen, Mika, et al.
(författare)
-
Epistemic logic, Cryptography, Logical Omniscience, BAN Logic
- 2005
-
Konferensbidrag (refereegranskat)abstract
- BAN logic is an epistemic logic for verifying cryptographic protocols. While BAN has been quite successful from a practical point of view, the semantics of the epistemic modality is unclear. Several Kripke semantics have been proposed, but they do not attempt at anything beyond a soundness result. Completeness is prevented by the so called logical omniscience problem: Agents in BAN can draw only feasibly computable consequences of their knowledge, whereas agents in Kripke semantics are not so constrained. To circumvent this problem, we index the epistemic possibility relation of Kripke semantics with a message renaming, relating how cipher texts at the current state correspond to cipher texts at the epistemically possible state. An agent is said to know a property of a message if corresponding messages at epistemically possible states satisfy that property. We obtain completeness with respect to message passing systems, and decidability, by transferring canonical model and filtration constructions from Kripke semantics.
|
|
| 3. |
- Cohen, Mika, et al.
(författare)
-
Logical Omniscience in the Semantics of BAN Logics
- 2005
-
Konferensbidrag (refereegranskat)abstract
- BAN logic is an epistemic logic for verification of cryptographic protocols. A number of semantics have been proposed for BAN logic, but none of them capture the intended meaning of the epistemic modality in a satisfactory way. This is due to the so-called logical omniscience problem : Agents are ”ideal reasoners” in existing semantics, while agents in BAN logic have only limited cryptographic reasoning powers. Logical omniscience is unavoidable in Kripke semantics, the standard semantical framework in epistemic logic. Our proposal is to generalize the epistemic accessibility relation of Kripke semantics so that it changes not only the current execution point, but also the currently predicated message. When nstantiated on message passing systems, the semantics validates BAN logic. It makes agents introspective (”self-aware”) of their own knowledge and of their own actions of sending, receiving and extracting.
|
|
| 4. |
- Cohen, Mika, 1971-
(författare)
-
Logics of Knowledge and Cryptography : Completeness and Expressiveness
- 2007
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
