We present a language for access control. The language is organized around the
notion of execution on behalf of a principal. This is characterized using an
indexed lax modality. Central to the language is the idea of manifest security –
accessing a resource requires presenting a proof of accessibility to the
resource monitor. Proofs are generated at runtime by actions such as typing in
password, looking up an access-control list or by composing other proofs etc. In
the present work, we consider a simplified setting in which the access-control
theory is static. In such a case proofs can be regarded as static
entities. Proof generation can be hoisted away from resource access since proofs
become permanent. Also, the actual proofs are irrelevant. The results of runtime
checks can therefore be reflected as types and the program can be verified
statically to ensure that relevant runtime checks would be passed before
accessing any resource. We prove a theorem stating that the language is safe in
terms of how all a principal can get to access a resource.