Name
Abstract | ||
|---|---|---|
In this paper, we improve on a previous result by Gagné et al. [9] for automatically proving the semantic security of symmetric modes of operation for block ciphers. We present a richer assertion language that uses more flexible invariants, and a more complete set of rules for establishing the invariants. In addition, all our invariants are given a meaningful semantic definition, whereas some invariants of the previous result relied on more ad hoc definitions. Our method can be used to verify the semantic security of all the encryption modes that could be proven secure in [9], in addition to other modes, such as Propagating Cipher-Block Chaining (PCBC). |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-27901-0_3 | FPS |
Keywords | Field | DocType |
propagating cipher-block chaining,meaningful semantic definition,richer assertion language,complete set,block cipher,encryption mode,block cipher mode,improved method,automated verification,symmetric mode,flexible invariants,semantic security,previous result | Symmetric-key algorithm,Chaining,Semantic security,Message authentication code,Block cipher,Block cipher mode of operation,Assertion,Theoretical computer science,Encryption,Mathematics | Conference |
Volume | ISSN | Citations |
6888 | 0302-9743 | 4 |
PageRank | References | Authors |
0.46 | 20 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Martin Gagné | 1 | 127 | 6.25 |
| Pascal Lafourcade | 2 | 569 | 58.37 |
| Yassine Lakhnech | 3 | 913 | 78.50 |
| Reihaneh Safavi-Naini | 4 | 2378 | 257.74 |