Symmetric encryption in a simulatable Dolev-Yao style cryptographic library
- 13 November 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Recently we showed how to justify a Dolev-Yao type model of cryptography as used in virtually all automated protocol provers under active attacks and in arbitrary protocol environments. The justification was done by defining an ideal system handling Dolev-Yao-style terms and a cryptographic realization with the same user interface, and by showing that the realization is as secure as the ideal system in the sense of reactive simulatability. This definition encompasses arbitrary active attacks and enjoys general composition and property-preservation properties. Security holds in the standard model of cryptography and under standard assumptions of adaptively secure primitives. A major primitive missing in that library so far is symmetric encryption. We show why symmetric encryption is harder to idealize in a way that allows general composition than existing primitives in this library. We discuss several approaches to overcome these problems. For our favorite approach we provide a detailed provably secure idealization of symmetric encryption within the given framework for constructing nested terms.Keywords
This publication has 19 references indexed in Scilit:
- Logics for reasoning about cryptographic constructionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- On the freedom of decryptionInformation Processing Letters, 2003
- Plaintext Awareness via Key RegistrationPublished by Springer Nature ,2003
- Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition ParadigmPublished by Springer Nature ,2000
- Encode-Then-Encipher Encryption: How to Exploit Nonces or Redundancy in Plaintexts for Efficient CryptographyPublished by Springer Nature ,2000
- Improved Non-committing Encryption Schemes Based on a General Complexity AssumptionPublished by Springer Nature ,2000
- Adaptively secure multi-party computationPublished by Association for Computing Machinery (ACM) ,1996
- Random oracles are practicalPublished by Association for Computing Machinery (ACM) ,1993
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Theory and application of trapdoor functionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982