Computationally secure information flow [Elektronische Ressource] / von Peeter Laud

Computationally Secure Information FlowDissertationZur Erlangung des Grades einesDoktors der Ingenieurwissenschaften (Dr.-Ing.)der Naturwissenschaftlich-Technischen Fakultat Ider Universitat des SaarlandesvonPeeter LaudSaarbruckenApril, 2002ISBN 9985-78-703-XTag des Kolloquiums: 16.09.2002Dekan: Prof. Dr. Philipp SlusallekGutachter: Prof. Dr. Reinhard WilhelmProf. Dr. Birgit P tzmannVorsitzender: Prof. Dr. Harald GanzingerAbstractThis thesis presents a de nition and a static program analysis forsecure information o w. The of secure information o w is notbased on non-interference, but on the computational independence ofthe program’s public outputs from its secret inputs. Such de nition al-lows cryptographic primitives to be gracefully handled, as their securityis usually de ned to be only computational, not information-theoretical.The analysis works on a simple imperative programming languagecontaining a cryptographic primitive|encryption|as a possible opera-tion. The analysis captures the intuitive qualities of the (lack of) infor-mation o w from a plaintext to its corresponding ciphertext. We provethe analysis correct with respect to the de nition of secure information o w described above. In the proof of correctness we assume that theencryption primitive hides the identity of plaintexts and keys.This thesis also considers the case where the identities of plaintextsand keys are not hidden by encryption, i.e.