Sciweavers

TARK
2007
Springer

Preservation of epistemic properties in security protocol implementations

14 years 10 days ago
Preservation of epistemic properties in security protocol implementations
We introduce (i) a general class of security protocols with private channel as cryptographic primitive and (ii) a probabilistic epistemic logic to express properties of security protocols. Our main theorem says that when a property expressed in our logic holds for an ideal protocol (where “ideal” means that the private channel hides everything), then it also holds when the private channel is implemented using an encryption scheme that guarantees perfect secrecy (in the sense of Shannon). Our class of protocols contains, for instance, an oblivious transfer protocol by Rivest and Chaum’s solution to the dining cryptographers problem, and in our logic we can express fundamental security properties of these protocols. The proof of the main theorem is based on a notion of refinement for probabilistic Kripke structures. Key words: security protocols, epistemic logic, preservation theorem.
Ron van der Meyden, Thomas Wilke
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TARK
Authors Ron van der Meyden, Thomas Wilke
Comments (0)