alert_some_login

exists is the sole quantifier: it asserts at least one satisfying assignment, with candidate values coming only from the atom that binds the variable. This policy permits an Alert if some user logged in to this Alert’s server within the last hour. The bound u is range-restricted by the Login predicate’s input.user field, and input.server: context.input.server pins the login’s server to the server named in the current Alert request.

The trace shows all the interesting cases (within 1h = 3600s, inclusive):

@0 — alice logs in to s1 (a Login, not an Alert; no permit applies) → deny.
@100 — bob alerts on s1; some user (alice) logged in to s1 100s ago → allow. Note exists is “at least one,” and the witness need not be the alerting principal — alice’s login satisfies bob’s alert.
@200 — bob alerts on s2; no login to s2 (the server pin fails) → deny.
@5000 — alice alerts on s1, but the only s1 login was 5000s ago, outside the 1h window → deny.

Referenced by guide/04-temporal-expressions.

Policy

// `exists` is the sole quantifier: it asserts at least one satisfying
// assignment, with candidate values coming only from the atom that binds the
// variable. Permit an Alert if SOME user logged in to this Alert's server
// within the last hour (the bound `u` is range-restricted by the Login field).
@id("alert_some_login")
permit (
    principal,
    action == Drupe::Action::"Alert",
    resource
)
when temporal {
    exists (u: String). formerly within 1h Drupe::Action::"Login"::request{ input.user: u, input.server: context.input.server }
};

Schema

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

  type AlertOutput = {  };

  type ContentFilterFinding = {
    severityScore: decimal
  };

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

  type LoginOutput = {  };

  type PromptAttackFinding = {
    severityScore: decimal
  };

  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 "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 "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")
@100 scope(principal: Drupe::OAuthUser::"bob", resource: Drupe::Gateway::"gw1") request_context(input: { level: 1, server: "s1" }) Drupe::Action::"Alert"::request(input: { level: 1, server: "s1" }, callerPrincipal: Drupe::OAuthUser::"bob", callerResource: Drupe::Gateway::"gw1", requestId: "u2")
@200 scope(principal: Drupe::OAuthUser::"bob", resource: Drupe::Gateway::"gw1") request_context(input: { level: 2, server: "s2" }) Drupe::Action::"Alert"::request(input: { level: 2, server: "s2" }, callerPrincipal: Drupe::OAuthUser::"bob", callerResource: Drupe::Gateway::"gw1", requestId: "u3")
@5000 scope(principal: Drupe::OAuthUser::"alice", resource: Drupe::Gateway::"gw1") request_context(input: { level: 3, server: "s1" }) Drupe::Action::"Alert"::request(input: { level: 3, server: "s1" }, callerPrincipal: Drupe::OAuthUser::"alice", callerResource: Drupe::Gateway::"gw1", requestId: "u4")

Expected Output

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

Event Schema

// Unpinned event schema.
//
// Same structure as the pinned default but WITHOUT pins. Temporal
// predicates use global-trace semantics: a policy can match events
// from any principal unless it explicitly constrains callerPrincipal.
//
// Use this to see the behavioral difference vs the pinned default:
//   dogwood replay --event-schema configuration/event-schemas/unpinned.dwschema ...

decision event <A>::request {
    ...inputs(A),
    callerPrincipal:   principalType(A),
    callerResource:    resourceType(A),
    requestId:         String,
    sessionId:         String,
}

event <A>::response {
    ...inputs(A),
    ...outputs(A),
    callerPrincipal:   principalType(A),
    callerResource:    resourceType(A),
    requestId:         String,
    sessionId:         String,
}

event <A>::error {
    ...inputs(A),
    callerPrincipal:   principalType(A),
    callerResource:    resourceType(A),
    requestId:         String,
    sessionId:         String,
}