read_since_login

Positive-left since within 1h: the left operand must have held continuously since the anchor. Permit a Read only if a Login by the same user has held continuously since a Login by that user within the last hour (left since within W right, the classic MFOTL left S right).

This is corpus case 0034_since_explicit, lifted verbatim.

What the trace shows

By the since semantics, left since within W right holds at the decision timepoint i only if the left operand (Login) holds at every step from just after the anchor through i itself. But the rule’s scope is action == Read, so every applicable decision point is a Read event — and a Read event is never a Login::request. The left operand therefore fails at the decision step, so the condition can never hold. This policy is structurally always-DENY — matching corpus 0034, whose reference outputs are all false. An ALLOW is not achievable for a faithful positive-left Login since Login guarding a Read; interleaving extra logins between the reads (verified against the CLI) does not change this.

The trace exercises the natural cases, all of which deny:

@0, @10 — two Logins by alice (history-only; the scope is Read, so no permit applies → deny).
@12, @20 — alice Reads within an hour of her logins. The anchor (Login) is in the window, but the left operand (Login) does not hold at the Read decision step, so the since is false → deny.
@30 — bob Reads with no prior login of his own → deny.

This is the intended contrast with the “open session” idiom (!left since …, corpus 0418/0547), where a negated left holds at the read step and the policy can allow.

Referenced by guide/04-temporal-expressions.md.

Policy

// `since` is a suffix on a conjunct: `left since within W right` holds when an
// anchor `right` occurred in the window and `left` held continuously from just
// after it through now. Permit a Read only if a Login by the same user has
// held continuously since a Login by that user within the last hour.
@id("read_since_login")
permit (
    principal,
    action == Drupe::Action::"Read",
    resource
)
when temporal {
    Drupe::Action::"Login"::request{ input.user: context.input.user }
    since within 1h
    Drupe::Action::"Login"::request{ input.user: context.input.user }
};

Schema

namespace Drupe {
  type AlertInput = {
    level: Long,
    server: String
  };

  type AlertOutput = {  };

  type ContentFilterFinding = {
    severityScore: decimal
  };

  type HeartbeatInput = {
    server: String
  };

  type HeartbeatOutput = {  };

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

  type LoginOutput = {  };

  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 "Alert" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: AlertInput,
      output?: AlertOutput,
      system: SystemContext
    }
  };

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

  action "Heartbeat" in [Action::"CallTool"] appliesTo {
    principal: [IamEntity, OAuthUser, UnauthenticatedUser],
    resource: [Gateway],
    context: {
      input: HeartbeatInput,
      output?: HeartbeatOutput,
      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 "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: { server: "s1", user: "alice" }) Drupe::Action::"Login"::request(input: { server: "s1", user: "alice" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u1")
@10 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { server: "s1", user: "alice" }) Drupe::Action::"Login"::request(input: { server: "s1", user: "alice" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u2")
@12 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { document: "doc1", user: "alice" }) Drupe::Action::"Read"::request(input: { document: "doc1", user: "alice" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u3")
@20 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { document: "doc1", user: "alice" }) Drupe::Action::"Read"::request(input: { document: "doc1", user: "alice" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u4")
@30 scope(principal: Drupe::OAuthUser::"bob", resource: Drupe::Gateway::"gw1") request_context(input: { document: "doc1", user: "bob" }) Drupe::Action::"Read"::request(input: { document: "doc1", user: "bob" }, callerPrincipal: Drupe::OAuthUser::"bob", callerResource: Drupe::Gateway::"gw1", requestId: "u5")

Expected Output

@0 (time point 0): DENY
@10 (time point 1): DENY
@12 (time point 2): DENY
@20 (time point 3): DENY
@30 (time point 4): DENY