Formal Modelling and Verification of Access Control Policies

Project: PHD

Description

We model Access Control Policies, mainly RBAC and policies expressed in XACML.
This model is used for automatic reasoning, and constructs attacks against faulty policies. Policies for Web sites can be sometimes extracted from their Java code,
or injected in their code.
AcronymTh-HTO
StatusFinished
Effective start/end date20/11/071/10/11

Keywords

  • Security
  • Formal Specification
  • Automated Verification
  • Access Control
  • Role-based Access Control (RBAC)