read_login_not_logout

The accepted “A but not B” idiom with restrictor-first conjunct ordering. A guarded negation (!B) restricts nothing, so it is legal only when a preceding conjunct in the same && chain already range-restricts its free variables. Here the restrictor comes first:

formerly within 1h Login{ input.user: context.input.user }   // restrictor
&& !Logout{ input.user: context.input.user }                 // guarded negation, after

Permit a Read only if the same user logged in within the last hour and has not since logged out. (Reversing the two conjuncts — negation before its restrictor — is the rejected form.)

The !Logout conjunct is an anti-join at the decision timepoint: the decision event is always a Read, so what drives the verdict in this trace is the formerly within 1h Login restrictor.

The trace shows both an allow and a deny:

• @0 — alice logs in (a Login event; no Read permit applies) -> deny.
• @100 — alice reads 100s after login (login still inside the 1h window) -> allow.
• @4000 — alice reads 4000s after login (login now outside the 1h window) -> deny.
• @4100 — bob reads with no prior login -> deny.

Referenced by guide/04-temporal-expressions.md (line 525, the accepted restrictor-first example).

Policy

// The accepted "A but not B" idiom with restrictor-first conjunct ordering: a
// guarded negation must come AFTER a conjunct that range-restricts its
// variables. Permit a Read only if the same user successfully logged in within
// the last hour AND has not since successfully logged out.
@id("read_login_not_logout")
permit (
    principal,
    action == Drupe::Action::"Read",
    resource
)
when temporal {
    formerly within 1h Drupe::Action::"Login"::response{ input.user: context.input.user }
    && !Drupe::Action::"Logout"::response{ input.user: context.input.user }
};

Schema

namespace Drupe {
  type ComputeInput = {
    user: String
  };

  type ComputeOutput = {  };

  type ContentFilterFinding = {
    severityScore: decimal
  };

  type LoginInput = {
    server: String,
    user: String
  };

  type LoginOutput = {  };

  type LogoutInput = {
    user: String
  };

  type LogoutOutput = {  };

  type PromptAttackFinding = {
    severityScore: decimal
  };

  type ReadInput = {
    document: String,
    user: String
  };

  type ReadOutput = {  };

  type SensitiveInfoFinding = {
    confidenceScore: decimal
  };

  type SystemContext = {
    now: datetime
  };

  entity Gateway;

  entity IamEntity = {
    id: String
  };

  entity OAuthUser = {
    id: String
  } tags String;

  entity UnauthenticatedUser;

  action "CallTool" in [Action::"Mcp"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "Compute" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: ComputeInput,
      output?: ComputeOutput,
      system: SystemContext
    }
  };

  action "Http" appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "InvokeAgent" in [Action::"Http"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input?: {      },
      system: SystemContext
    }
  };

  action "InvokeLLM" in [Action::"Http"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input?: {      },
      system: SystemContext
    }
  };

  action "Login" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: LoginInput,
      output?: LoginOutput,
      system: SystemContext
    }
  };

  action "Logout" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: LogoutInput,
      output?: LogoutOutput,
      system: SystemContext
    }
  };

  action "Mcp" appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };

  action "Read" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: ReadInput,
      output?: ReadOutput,
      system: SystemContext
    }
  };

  action "UnknownTool" in [Action::"CallTool"] appliesTo {
    principal: [OAuthUser, IamEntity, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      system: SystemContext
    }
  };
}

Trace

@0 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { user: "alice", server: "s1" }) Drupe::Action::"Login"::request(input: { user: "alice", server: "s1" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u1")
@5 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { user: "alice", server: "s1" }) Drupe::Action::"Login"::response(input: { user: "alice", server: "s1" }, output: { result: true }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u1")
@100 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { user: "alice", document: "doc1" }) Drupe::Action::"Read"::request(input: { user: "alice", document: "doc1" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u2")
@4000 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { user: "alice", document: "doc4" }) Drupe::Action::"Read"::request(input: { user: "alice", document: "doc4" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u3")
@4100 scope(principal: Drupe::OAuthUser::"bob", resource: Drupe::Gateway::"gw1") request_context(input: { user: "bob", document: "doc2" }) Drupe::Action::"Read"::request(input: { user: "bob", document: "doc2" }, callerPrincipal: Drupe::OAuthUser::"bob", callerResource: Drupe::Gateway::"gw1", requestId: "u4")

Expected Output

@0 (time point 0): DENY
@100 (time point 1): ALLOW  [rules: 0]
@4000 (time point 2): DENY
@4100 (time point 3): DENY