Next:
Contents
Contents
Proof carrying authorization in ML5
Romain Brenguier
Internship report
April - August 2008
Supervisor : Frank Pfenning
Contents
Synthesis
General context
Problem Studied
Proposed contribution
Validity arguments
Achievements and Prospects
Introduction
Proof carrying authorization
Access control
Authorization logic
Example
Proof carrying authorization architecture
ML5
A modal logic for distributed computing
IS5
Lambda 5 natural deduction
Validity
Implementation
A compiler : ml5pgh
Web Features
Example
Security issues
ML5 with Proof Carrying Authorization
Introduction
Architecture
Authorization logic
Syntax of the language
Explicit polymorphism
Read and Write
Certificates
Implementation
Runtime system
Identity
Certificates
Resources
Application
Example : grade sheet
Conclusion
Bibliography
About this document ...
brenguier 2008-08-25