A design for a security-typed language with certificate-based declassification

Abstract

This paper presents a calculus that supports information-flow security policies and certificate-based declassification. The decentralized label model and its downgrading mechanisms are concisely expressed in the polymorphic lambda calculus with subtyping (System F-≺). We prove a conditioned version of the noninterference theorem such that authorization for declassification is justified by digital certificates from public-key infrastructures. © Springer-Verlag Berlin Heidelberg 2005.