Conference paper review system (CRS)
This case study defines a simple policy for a conference review system. In CRS, chair can assign reviewers to the papers, reviewers can assign subreviewers to their reviewing papers, and reviewers are not able to read other reviewers submitted review, unless they have submitted their own. pc members can read the reviews of a paper if they are not already assigned as the reviewer of that paper (script file is available here).
Query: The query asks if a strategy exists such that PC member a first can read the review of the reviewer b for the paper p and then collaborating with chair a, submit a review for p.
The tool outputs the following strategy (with some changes for more readability):
[a]: (no action) [a, c]: Agent c performs addReviewer(a,p); Agent a performs submitreview(a,p); Goal;
Strategy says: For the first goal, no action needs to be taken. Agent a, as a pc member, is able to read the review of the agent b at the initial states. Now, c assigns a as the reviewer of the paper p, and then, c submits his review for p (A security hole in the policy discovered).
Student information service (SIS)
In student information system, a lecturer can assign a student as the demonstrator of another one, if he is higher than the other. System enforces authorization policies for marking students and accessing the marks (script file is available
here).
Query: The query checks if any situation in the system exists such that two students can be assigned as each other's demonstrator.
The tool states that SIS does not satisfy this specification.
Changing password policy
This policy is illustrated in technical report (Example 4) to demonstrated how the model-checking algorithm works. We have added to extra predicates to show how knowledge-based verification works (script file is available here).
Query: The query looks for any strategy that lets a user to change his password.
The tools outputs two strategies
[1]: Agent 1 performs setY(1); Agent 1 performs setX(1);
(Guess):if (changePassPerm(1) is true) {Agent 1 performs setchangePass(1); Goal;}
else {Agent 1 performs setTrick(1); Agent 1 performs setchangePass(1); Goal;}
[1]: Agent 1 performs setX(1); Agent 1 performs setY(1)
if (changePassPerm(1) is true) {Agent 1 performs setchangePass(1); Goal;}
else {Agent 1 performs setTrick(1); Agent 1 performs setchangePass(1); Goal;}
The strategies show that an agent has two different ways to change his password. The second on is not risky, as in the decision state, agent does not need to guess the value of changePassPerm(1), because he already knows its value.
Employee information system (EIS)
The policy for employee information system enforces several rules for bonus allocation. Managers are able to set and read the bonus for the employers, but they are not permitted to set the bonus for other managers or directors. (script file is available here).
Query: The query asks if there is any strategy so that a manager can set a bonus for the other one.
The tools provide a strategy for agents 1 and 2 as two managers :
[1, 2]: Agent 1 performs delManager(1); Agent 2 performs addBonus(1,1); Goal;
So, if manager 1 resigns as manager, then manager 2 can set a bonus for 1 (it is up to policy designer to decide if such a situation is acceptable in the organization or not).
