### Skapa referens, olika format (klipp och klistra)

**Harvard**

Askarov, A., Hedin, D. och Sabelfeld, A. (2008) *Cryptographically-Masked Flows*.

** BibTeX **

@article{

Askarov2008,

author={Askarov, Aslan and Hedin, Daniel and Sabelfeld, Andrei},

title={Cryptographically-Masked Flows},

journal={Theoretical Computer Science},

issn={0304-3975},

volume={402},

issue={2-3},

pages={82-101},

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 article 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 nonkeys), which we exemplify with secure implementations of cryptographic protocols. Because the model is based on a standard noninterference property, it allows us to develop some natural extensions. In particular, we consider public-key cryptography and integrity, which accommodate reasoning about primitives that are vulnerable to chosen-ciphertext attacks.},

year={2008},

keywords={Cryptography; Information flow; Language-based security; Noninterference; Security type systems},

}

** RefWorks **

RT Journal Article

SR Electronic

ID 79624

A1 Askarov, Aslan

A1 Hedin, Daniel

A1 Sabelfeld, Andrei

T1 Cryptographically-Masked Flows

YR 2008

JF Theoretical Computer Science

SN 0304-3975

VO 402

IS 2-3

SP 82

AB 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 article 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 nonkeys), which we exemplify with secure implementations of cryptographic protocols. Because the model is based on a standard noninterference property, it allows us to develop some natural extensions. In particular, we consider public-key cryptography and integrity, which accommodate reasoning about primitives that are vulnerable to chosen-ciphertext attacks.

LA eng

DO 10.1016/j.tcs.2008.04.028

LK http://publications.lib.chalmers.se/records/fulltext/local_79624.pdf

OL 30