Implementation and verification of programmable security. This paper presents a methodology for augmenting programming languages with configurable security services. In particular, it describes JPAC, a Java extension that provides syntax for expressing discretionary package-based access control. Access control is based on a variation of a ticket-based authorization model. The authorization model has been succesfully implemented in the Isabelle theorem proving environment. Moreover, a novel cryptographic verification formalism is used to analyze JPAC’s secure method invocation protocol. Programmable security architectures and cryptographic protocol verification formalisms used in concert can provide verifiably secure programming systems for Internet applications.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Magill, Stephen; Skaggs, Bradley; Papa, Mauricio; Hale, John: Implementation and verification of programmable security (2003)