I wonder if someone could direct me to a basic introduction to formal methods applied to role-based security.  I'm particularly interested in the question of formal verification and the kind of mathematical abstractions that would appropriately address confidentiality and / or conflicts of interest that arise from overlapping roles in a SSO (single sign-on) system.  Thanks much in advance.PS I'm asking this question in parallel w/ conducting my own literature search.
Formal Methods Applied to Role-Based Security (RBAC)
lo.logic;security;formal methods
My knowledge is a bit stale, as I haven't actively researched this field in the last couple of years. None of these is probably the state of the art, but a good place to start looking backwards (i.e., chase references) and forwards (i.e., see who cites it).If you're looking into information flow (making sure classified information doesn't leak to untrusted roles), a reasonable place to start is Martin Abadi et al's Dependency Core Calculus. I think it's reasonable enough that anyone who does formal methods in the area would refer to it (directly, or once removed).If you're looking into access control/authorisation (role A says role B controls the data, role B says you can access the data, etc.), Abadi recently published a tutorial book chapter on the subject, so might be a good place to start.If you're looking into authentication (whether the agent saying he is A is indeed A), I defer to someone else. I'll try to have a look later. 