Abstract On the Computational Soundness of Cryptographically Masked Flows

To speak about the security of information flow in programs employing cryptographic operations, definitions based on computational indistinguishability of distributions over program states have to be used. These definitions, as well as the accompanying analysis tools, are complex and error-prone to argue about. Cryptographically masked flows, proposed by Askarov, Hedin and Sabelfeld, are an abstract execution model and security definition that attempt to model is useful because analysis of programs can be conducted using the usual techniques for enforcing non-interference. model is computationally sound, i.e. when does the security of a program in their model imply the computational security of this program. This paper spells out a reasonable set of conditions and then proposes a simpler abstract model that is nevertheless no more restrictive than the cryptographically masked flows together with these conditions for soundness