(*
   Specification of subject-driven credential discovery.
*)

(* use forward-chaining ismem specification *)
#include "ismem_forwards.lo".


entry : entity -> role_name -> role_expr -> o.


subject : list role_expr -> entity -> role_name -> o.
subject ((role A Ra)::Res) A Ra. 
subject (X::Res) A Ra <= subject Res A Ra. 


credential A Ra Re, 
entry B Rb (role A Ra) -o 
{!credential B Rb (role A Ra)}. 

credential A Ra Re, 
entry B Rb (^ A) -o 
{!credential B Rb (^ A)}. 

credential A Ra Re, 
ismem (role D R) A, 
entry B Rb (linked_role D R Ra) -o 
{!credential B Rb (linked_role D R Ra)}. 

credential A Ra Re, 
entry B Rb (inter Res), 
subject Res A Ra -o 
{!credential B Rb (inter Res)}. 


seed : role_expr -> entity -> 
           entity -> role_name -> role_expr -> o. 
seed R A B Rb (^ A) o- entry B Rb (^ A).


auth : role_expr -> entity -> o. 
auth R A o- ismem R A, top. 
auth R A o- 
  seed R A B Rb RE, 
  (credential B Rb RE => {auth R A}).