Formal Methods Applied to Role-Based Security (RBAC) 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.
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.