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.

• Type: Conference
• Year: 2007
• Where: TARK
• Authors: Ron van der Meyden, Thomas Wilke
• Keywords: Epistemic Logic, Private Channel, Security Protocols, TARK 2007