<p>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).</p>

<p>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 <a href="http://dl.acm.org/citation.cfm?doid=292540.292555" rel="nofollow">Dependency Core Calculus</a>. I think it's reasonable enough that anyone who does formal methods in the area would refer to it (directly, or once removed).</p>

<p>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 <a href="http://www.springerlink.com/content/87428t143533142q/?MUD=MP" rel="nofollow">tutorial book chapter</a> on the subject, so might be a good place to start.</p>

<p>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. </p>

CC BY-SA 3.0
2012-09-18T17:27:48.870Z
2012-09-18T17:27:48.870Z
Ohad Kammar
<p>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.</p>

<p>PS I'm asking this question in parallel w/ conducting my own literature search.</p>

<lo.logic><security><formal-methods>
Formal Methods Applied to Role-Based Security (RBAC)
user10756
# Formal Methods Applied to Role-Based Security (RBAC)

(Asked by: username_0 on 2012-09-17)

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.

**Tags:** lo.logic, security, formal-methods


---

## 1 answers

### Answer by username_1 on 2012-09-18. Score: 4 | Accepted answer

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](http://dl.acm.org/citation.cfm?doid=292540.292555). 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](http://www.springerlink.com/content/87428t143533142q/?MUD=MP) 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.


---

