Tse, StephenZdancewic, Stephan A2023-05-222023-05-222005-04-012006-04-05https://repository.upenn.edu/handle/20.500.14332/6271This 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.Presentation