Cryptographically-masked flows

Abstract. Cryptographic operations are essential for many security-critical systems. Reasoning about information flow in such systems is challenging because typical (noninterference-based) information-flow definitions allow no flow from secret to public data. Unfortunately, this implies that programs with encryption are ruled out because encrypted output depends on secret inputs: the plaintext and the key. However, it is desirable to allow flows arising from encryption with secret keys provided that the underlying cryptographic algorithm is strong enough. In this paper we conservatively extend the noninterference definition to allow safe encryption, decryption, and key generation. To illustrate the usefulness of this approach, we propose (and implement) a type system that guarantees noninterference for a small imperative language with primitive cryptographic operations. The type system prevents dangerous program behavior (e.g., giving away a secret key or confusing keys and non-keys), ...

• Type: Journal
• Year: 2008
• Where: TCS
• Authors: Aslan Askarov, Daniel Hedin, Andrei Sabelfeld
• Keywords: Cryptographic Operations, Primitive Cryptographic Operations, Secret Key, TCS 2008, Theoretical Computer Science