Security proof with dishonest keys

Security proof with dishonest keys. Hubert Comon-Lundh, Véronique Cortier, and Guillaume Scerri. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12), pp. 149–168, Lecture Notes in Computer Science 7215, Springer, Tallinn, Estonia, March 2012.

Download

[PDF] [long version] [HTML]

Abstract

Symbolic and computational models are the two families of models for rigorously analysing security protocols. Symbolic models are abstract but offer a high level of automation while computational models are more precise but security proof can be tedious. Since the seminal work of Abadi and Rogaway, a new direction of research aims at reconciling the two views and many soundness results establish that symbolic models are actually sound w.r.t. computational models.
This is however not true for the prominent case of encryption. Indeed, all existing soundness results assume that the adversary only uses honestly generated keys. While this assumption is acceptable in the case of asymmetric encryption, it is clearly unrealistic for symmetric encryption. In this paper, we provide with several examples of attacks that do not show-up in the classical Dolev-Yao model, and that do not break the IND-CPA nor INT-CTXT properties of the encryption scheme. Our main contribution is to show the first soundness result for symmetric encryption and arbitrary adversaries. We consider arbitrary indistinguishability properties and an unbounded number of sessions. This result relies on an extension of the symbolic model, while keeping standard security assumptions: IND-CPA and IND-CTXT for the encryption scheme.

BibTeX

@inproceedings{post12-clefs,
doi = {10.1007/978-3-642-28641-4_9},
   address = {Tallinn, Estonia}, 
   author = {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique and Scerri, Guillaume}, 
   booktitle = {{P}roceedings of the 1st {I}nternational {C}onference on {P}rinciples of {S}ecurity and {T}rust ({POST}'12)}, 
   month = mar, 
   publisher = {Springer}, 
   series = {Lecture Notes in Computer Science}, 
   title = {Security proof with dishonest keys}, 
   volume    = {7215},
  pages     = {149--168},
   year = {2012}, 
   abstract = {Symbolic and computational models are the two families of models for rigorously analysing security protocols. Symbolic models are abstract but offer a high level of automation while computational models are more precise but security proof can be  tedious.
Since the seminal work of Abadi and Rogaway, a new direction of research aims at reconciling the two views and many soundness results establish that symbolic models are actually sound w.r.t. computational models. 
\par
This is however not true for the prominent case of encryption. Indeed, all existing soundness results assume that the adversary only uses honestly generated keys. While this assumption is acceptable in the case of asymmetric encryption, it is clearly unrealistic for symmetric encryption.
In this paper, we provide with several examples of attacks that do not show-up in the classical Dolev-Yao model, and that do not break
the IND-CPA nor INT-CTXT properties of the encryption scheme. 
Our main contribution is to show the first soundness result for symmetric encryption and arbitrary adversaries.
We consider arbitrary indistinguishability properties and an unbounded number of sessions. 
This result relies on an extension of the symbolic model, while keeping standard security assumptions:
IND-CPA and IND-CTXT for the encryption scheme. },
}