Individual Access Management (IAM) — Functional Specification

Date: 2026-02-16 Branch: iam-specification Status: Draft v2.1 Dafny source: apps/specifications/dafny/iam/main.dfy Model: PARC request, flat permit/deny (based on Cedar authorization model)

---

1. Core Function

The entire IAM system reduces to one function:

checkAccess(principal, action, resource, context) → Allow | Deny

Every request is a PARC tuple:

Component	Type	Description	Example
Principal	{userId, orgId}	The authenticated user making the request	{userId: "f47ac10b-...", orgId: "org-123"}
Action	string	The operation being performed	"read", "write", "admin"
Resource	string	The target of the operation	"store.products", "org.members"
Context	map<string, string>	Optional request metadata for future conditions	{storeId: "store-456", ip: "10.0.0.1"}

Everything else — policies, roles, groups, tables — exists to resolve that answer.

This is the conceptual API exposed by IamService. Internally, IamService resolves the principal's policies from the database and delegates to the compiled Dafny engine, which has a narrower signature (see Section 11.3).

---

2. Resolution Inputs

When a PARC request arrives, the engine collects all applicable policies, then evaluates:

request(principal, action, resource, context)
  → principal.orgId
      → user's roleIds[]
          → Role { groupIds[] }
              → Group { policyIds[] }
                  → Policy { effect: Permit|Deny, resource, action, conditions }

Minimum inputs to the decision function

Input	Description	Example
principal	Who is asking (userId + orgId)	{userId: "f47ac10b-...", orgId: "org-123"}
action	What operation	"write", "read", "admin"
resource	What target	"store.products", "org.members"
context	Optional metadata	{storeId: "store-456"}

Minimum state the function reads

State	Resolved from	Example
User's roleIds	userId → iam_user_roles	["role-1", "role-2"]
Each role's groupIds	roleId → iam_role_groups	role-1 → ["group-1", "group-2"]
Each group's policyIds	groupId → iam_group_policies	group-1 → ["policy-1", "policy-2"]
Each policy's effect + scope	policyId → iam_policies	Permit("store.products", "write")

---

3. Resolution Algorithm

Three rules. No priority levels, no modifiers, no special cases.

Step 1. Collect all policies reachable by this user:
          policies = union of policies from all groups from all roles

Step 2. Filter to policies that match the request:
          matching = policies where policyMatches(policy, request) is true
          (skip any policy that errors during evaluation)

Step 3. Apply flat resolution:
          a. If any matching policy has effect = Deny  → return DENY.
          b. Else if any matching policy has effect = Permit → return ALLOW.
          c. Else → return DENY.                        (default deny)

Matching Rules

A policy matches a request if both of the following are true:

resourceMatches(policy.resource, request.resource):
    policy.resource == "*" OR policy.resource == request.resource

actionMatches(policy.action, request.action):
    policy.action == "*" OR policy.action == request.action

Matching is exact string equality or the literal "*" wildcard. There is no glob matching, no prefix matching, no regular expression. "store.*" does NOT match "store.products" — it is an invalid resource string. "*" is the only wildcard and it matches any value.

Resolution Summary

Any deny policy matches   →  DENY
Any permit policy matches →  ALLOW
No policy matches         →  DENY  (default deny)

Deny always wins. This is unconditional — there is no override mechanism, no priority ordering between deny and permit beyond "deny wins."

Skip-on-error

If a policy cannot be evaluated (malformed condition, missing data, type error), that policy is skipped. A skipped policy never contributes a Permit. This ensures errors cannot produce false allows.

In v2, conditions are not evaluated (see Section 4.1), so skip-on-error only triggers on structural errors: a policy with a null effect, resource, or action field. The property is defined now so it holds when conditions are implemented in a future version.

---

4. Type System

4.1 Core Types

Effect = Permit | Deny

Condition = {
    -- Reserved for future use (e.g. time-of-day, IP range, storeId matching).
    -- In v2, conditions are always empty. A policy with an empty condition list
    -- matches unconditionally. A policy with a non-empty condition list is skipped
    -- (skip-on-error) until the condition evaluator is implemented.
}

EvaluationError = {
    policyId:   PolicyId
    message:    string              -- human-readable description of what went wrong
}

Policy = {
    id:         PolicyId
    effect:     Effect
    resource:   string              -- e.g. "store.products", "*" for wildcard
    action:     string              -- e.g. "read", "write", "*" for wildcard
    conditions: list<Condition>     -- v2: always empty (see above)
}

Group = {
    id:         GroupId
    orgId:      OrganizationId      -- groups are org-scoped
    name:       string
    groupType:  SystemDefined | UserDefined
    policies:   set<PolicyId>
}

Role = {
    id:         RoleId
    name:       string
    orgId:      OrganizationId
    groups:     set<GroupId>
}

User = {
    id:         UserId
    orgId:      OrganizationId
    roleIds:    set<RoleId>
}

4.2 Interface Types

Principal = {
    userId:     UserId
    orgId:      OrganizationId
}

Request = {
    principal:  Principal
    action:     string
    resource:   string
    context:    map<string, string>
}

Response = {
    decision:            Permit | Deny
    determiningPolicies: set<PolicyId>      -- which policies caused the decision
    errors:              list<EvaluationError>  -- any policies that were skipped
    reason:              string              -- human-readable explanation for audit
}

4.3 Dropped Types (from v1)

Type	Why dropped
ModifierType	No modifier system in flat model
Modifier / PermissionModifier	Replaced by deny policies
ResolvedVia	Derivable from determiningPolicies in Response
isActive (on Role, User)	Handled at the application layer outside IAM (soft-delete, admin queries)

Anything that was an Override modifier becomes a deny policy. Anything that was a GrantAdditional modifier becomes a permit policy. Revoke modifiers become deny policies. The flat model subsumes all modifier use cases.

---

5. Properties Dafny Must Prove

Five properties. Everything else is optional.

P1. Default Deny

If no permit policy matches the request, the result is DENY.

forall request, policies:
    noPermitMatches(request, policies) ==>
        checkAccess(request, policies).decision == Deny

This is the foundation. Access is denied unless explicitly granted.

P2. Deny Overrides Permit

If any deny policy matches the request, the result is DENY — regardless of how many permit policies also match.

forall request, policies:
    anyDenyMatches(request, policies) ==>
        checkAccess(request, policies).decision == Deny

This is unconditional. There is no mechanism to override a deny.

P3. Skip-on-Error Safety

A policy that errors during evaluation never contributes a Permit to the decision.

forall request, policy, policies:
    evaluationError(policy, request) ==>
        policy.id not in checkAccess(request, policies).determiningPolicies

Errors are conservative — they can only reduce access, never expand it. In v2, an error is: a policy with non-empty conditions (since the condition evaluator is not implemented), or a policy with null/missing required fields.

P4. Determinism

Same request against the same policy set always produces the same decision.

forall request, policies:
    checkAccess(request, policies) == checkAccess(request, policies)

No randomness, no ordering dependency. The function is pure.

P5. Organization Boundary

Policies from other organizations cannot grant access to a user. A user's roles must all belong to their organization. A role's groups must all belong to the same organization as the role. A group's policies must all belong to the same organization as the group.

forall user, role:
    role in user.roleIds ==> role.orgId == user.orgId

forall role, group:
    group in role.groups ==> group.orgId == role.orgId

forall group, policy:
    policy in group.policies ==> policy.orgId == group.orgId

This is a structural invariant enforced on write (CreateUser, AddRoleToUser, AddGroupToRole, AddPolicyToGroup), not checked at decision time. The entire chain — user → roles → groups → policies — is confined to a single organization.

Dropped Properties (from v1)

Property	Why dropped
Role monotonicity	Was a property of the modifier system — in the flat model, adding a role that contains a deny policy CAN reduce access. This is correct behavior.
Override-is-absolute	No override mechanism in flat model
Revoke-beats-grant	No modifier priority in flat model — subsumed by P2 (deny overrides permit)

---

6. What Dafny Does NOT Handle

Concern	Why excluded
Firebase UID → userId mapping	Authentication, not authorization
How data enters the DB	API layer / controller concern
Membership tables (org_memberships, store_memberships)	Inputs to role assignment and store-scoped gating (see Section 7.1), not part of the IAM decision
Store-scoped membership checks	Pre-IAM gate, see Section 7.1
Caching	Implementation optimization
Feature flags	Deployment concern
Rate limiting, App Check, null byte sanitization	Separate security filters
Audit logging	Application-layer concern (see Section 12)

---

7. Integration Architecture

7.1 Store-Scoped Access (Hybrid Model)

Store-scoped requests require two checks in sequence:

1. Membership gate (existing AuthorizationService logic, unchanged): "Is this user a member of this store, OR an org admin of the parent org?" This reads store_memberships and org_memberships. If the user has no relationship to the store, return 403 immediately. IAM is never called.

2. Permission check (new IAM): "Does this user have store.products:write permission?" This runs the PARC evaluation. It reads the user's roles → groups → policies and runs the flat deny-overrides-permit algorithm.

Controller:
  authorizationService.requireStoreAccess(storeId, authUser)   // gate: membership
  iamService.checkAccess(authUser, "store.products", "write")  // fine-grained: permission

Why hybrid: The context field in PARC requests is reserved for future conditions. Until conditions are implemented, IAM alone cannot scope a user's permissions to a specific store. The membership gate provides store-level isolation; IAM provides fine-grained permission control within that gate.

When conditions are implemented: The membership gate can be removed. Store-scoped access becomes a single IAM call with context={storeId} and a condition like context.storeId in principal.storeIds.

Org-scoped requests do NOT need the hybrid model. The principal's orgId is part of the PARC tuple, and P5 (org boundary) ensures all policies belong to the same org.

7.2 Compilation Model

The Dafny spec compiles directly to Java:

dafny build --target:java iam.dfy → IamDecisionEngine.java

The verified Dafny code IS the production IamDecisionEngine. There is no separate "Java implementation" that must be kept in sync — the Dafny compiler generates the Java code, and the proofs guarantee its correctness.

DAFNY (source of truth)                  JAVA (compiled output)
────────────────────────                  ─────────────────────
iam.dfy                                  IamDecisionEngine.java (generated)
  ├── checkAccess()            ──dafny──►   ├── checkAccess() (verified)
  ├── Policy datatype          build──►     ├── Policy class (generated)
  ├── Request datatype                      ├── Request class (generated)
  └── Response datatype                     └── Response class (generated)

7.3 Hand-Written Java Wrappers

Any Java code that wraps the compiled Dafny engine (e.g., IamService that fetches data from the DB and calls the engine) is not formally verified. To validate these wrappers:

• DRT (differential random testing): Generate random PARC requests, run them through both the Dafny reference implementation and the Java wrapper, assert identical results.
• Unit tests: Standard JUnit tests for DB queries, request construction, error handling.

7.4 Two-Level checkAccess Distinction

The spec defines checkAccess at two levels:

Level	Signature	Implemented by
Conceptual API	checkAccess(principal, action, resource, context) → Allow | Deny	IamService (hand-written Java)
Decision engine	checkAccess(Request, Set<Policy>) → Response	IamDecisionEngine (compiled Dafny)

The conceptual API (Section 1) is what controllers call. IamService resolves the principal's policies from the database, constructs a Request, and delegates to the compiled decision engine. The decision engine is a pure function — it receives prefetched policies and returns a Response. It does no I/O.

7.5 Target State (IAM with PARC)

Controller
  → [if store-scoped] authorizationService.requireStoreAccess(storeId, authUser)
  → iamService.checkAccess(authUser, action, resource, context)
    → resolve userId from authUser
    → resolve orgId from request context
    → fetch user's roles from iam_user_roles
    → fetch groups from iam_role_groups for each role
    → fetch policies from iam_policies via iam_group_policies for each group
    → call IamDecisionEngine.checkAccess(request, policies)  ← compiled Dafny
    → return Response { decision, determiningPolicies, errors, reason }
    → 403 or proceed

7.6 Mapping Current AuthorizationService Methods to PARC

Current method	Store gate	PARC request
requireOrgMember(orgId, authUser)	No	(principal={userId, orgId}, action="read", resource="org.members", context={})
requireOrgAdmin(orgId, authUser)	No	(principal={userId, orgId}, action="admin", resource="org", context={})
requireStoreAccess(storeId, authUser)	Yes	(principal={userId, orgId}, action="read", resource="store", context={storeId})
requireStoreAdmin(storeId, authUser)	Yes	(principal={userId, orgId}, action="admin", resource="store", context={storeId})

The membership tables (org_memberships, store_memberships) serve two purposes:

1. Store gate: store_memberships is the pre-IAM membership check for store-scoped requests (Section 7.1).
2. Role assignment input: A user's membership maps to iam_user_roles rows. They are no longer the authorization mechanism for fine-grained permissions.

---

8. Database Tables

Six tables. The iam_user_modifiers table from v1 is dropped. A new iam_policies table replaces iam_group_permissions. Groups are org-scoped.

iam_policies (
    policy_id   UUID PRIMARY KEY,
    org_id      UUID NOT NULL REFERENCES organizations(org_id),
    effect      TEXT NOT NULL,             -- 'permit' | 'deny'
    resource    TEXT NOT NULL,             -- e.g. 'store.products', '*'
    action      TEXT NOT NULL,             -- e.g. 'read', 'write', '*'
    conditions  JSONB DEFAULT '[]',        -- reserved for future use (v2: always '[]')
    description TEXT,                      -- human-readable purpose
    created_at  TIMESTAMPTZ DEFAULT CURRENT_TIMESTAMP,
    UNIQUE (org_id, effect, resource, action)
)

iam_groups (
    group_id    UUID PRIMARY KEY,
    org_id      UUID NOT NULL REFERENCES organizations(org_id),
    name        TEXT NOT NULL,
    group_type  TEXT NOT NULL,             -- 'system' | 'user_defined'
    created_at  TIMESTAMPTZ DEFAULT CURRENT_TIMESTAMP
)

iam_group_policies (
    group_id    UUID REFERENCES iam_groups(group_id),
    policy_id   UUID REFERENCES iam_policies(policy_id),
    PRIMARY KEY (group_id, policy_id)
)

iam_roles (
    role_id     UUID PRIMARY KEY,
    org_id      UUID NOT NULL REFERENCES organizations(org_id),
    name        TEXT NOT NULL,
    created_at  TIMESTAMPTZ DEFAULT CURRENT_TIMESTAMP
)

iam_role_groups (
    role_id     UUID REFERENCES iam_roles(role_id),
    group_id    UUID REFERENCES iam_groups(group_id),
    PRIMARY KEY (role_id, group_id)
)

iam_user_roles (
    user_id     UUID REFERENCES merchant_users(user_id),
    role_id     UUID REFERENCES iam_roles(role_id),
    PRIMARY KEY (user_id, role_id)
)

Uniqueness Constraint on iam_policies

UNIQUE (org_id, effect, resource, action) means an org can have at most one permit policy and one deny policy per resource:action pair. This is intentional for v2 — policies are structural (one permit per resource:action, one deny per resource:action). When conditions are implemented in a future version, this constraint should be relaxed to allow multiple policies with different conditions for the same resource:action.

Changes from v1

v1	v2	Reason
iam_group_permissions	iam_policies + iam_group_policies	Policies are first-class entities, referenced by groups via junction table
iam_user_modifiers	(dropped)	No modifier system — deny policies replace all modifier use cases
iam_user_groups	(dropped)	Direct group assignment removed — all access flows through roles
iam_groups (no org_id)	iam_groups (with org_id)	Groups are org-scoped to enforce P5 org boundary through the full chain

---

9. Resource:Action Catalog

The complete set of (resource, action) pairs that the IAM system recognizes. Each corresponds to a controller method or group of methods.

Organization-Scoped Resources

Resource	Actions	Controller
org	read, write, admin	(org-level operations)
org.members	read, write, admin	OrgMemberController
org.invites	read, write, admin	OrgInviteController
org.categories	read, write, admin	CategoryController
org.suppliers	read, write, admin	SupplierController
org.activity	read	OrgActivityLogController

Store-Scoped Resources

Resource	Actions	Controller
store	read, write, admin	(store-level operations)
store.members	read, write, admin	StoreMemberController
store.invites	read, write, admin	StoreInviteController
store.products	read, write, admin	ProductController
store.inventory	read, write	InventoryController
store.serials	read, write	OrgSerialNumberController
store.transfers	read, write	StockTransferController
store.transactions	read, write, void	TransactionController
store.returns	read, write	ReturnController
store.batches	read, write, settle	BatchController
store.discounts	read, write, admin	DiscountController
store.promotions	read, write, admin	PromotionController
store.tax	read, write	TaxConfigController
store.compliance	read, write	ComplianceController
store.shifts	read, write, admin	ShiftController
store.customers	read, write	CustomerController
store.notifications	read, write	NotificationController
store.activity	read	StoreActivityLogController
store.reports	read	ReportController
store.settings	read, write	SettingsController
store.terminals	read, write, admin	TerminalController
store.query	read	QueryController
store.mkonnekt	read, write	MkonnektController
store.onboarding	read, write	OnboardingController
store.pins	write	UserPinController

Auth Resources

Resource	Actions	Controller
auth	login, read, write	AuthController

auth:login is a public action (no IAM check required). auth:read (/me) and auth:write (change password) are granted to any authenticated user regardless of role — they are implicit permits, not stored as policies.

---

10. Default Role → Policy Mapping

These are the system-defined roles created per-org when an organization is created. Each role maps to a group of permit policies. No default roles require deny policies — the absence of a permit policy is sufficient for default deny.

Role	Permit Policies
org_owner	All (resource, action) pairs — permit all
org_admin	All (resource, action) pairs — permit all
org_member	org.members:read, org.invites:read, org.categories:read, org.suppliers:read
store_admin	All store.* (resource, action) pairs
store_manager	All store.* except *.admin actions
store_cashier	store.products:read, store.inventory:read, store.transactions:*, store.returns:*, store.discounts:read, store.compliance:*, store.customers:*, store.shifts:read
stocker	store.products:read, store.inventory:*, store.serials:*, store.transfers:*, store.shifts:read

Seeding Strategy

System-defined data is seeded at two points:

On application startup (global, once):

• iam_policies: One row per (resource, action, effect=permit) pair from the catalog (Section 9). These are org-scoped, so they are created per-org (see below).

On organization creation (per-org):

1. Create iam_policies rows for all catalog entries, scoped to the new org.
2. Create one iam_groups row per default role (e.g., org_owner_default_group), scoped to the new org.
3. Create iam_group_policies links mapping each group to its permit policies per the table above.
4. Create one iam_roles row per default role, scoped to the new org.
5. Create iam_role_groups links mapping each role to its default group.
6. Create iam_user_roles rows assigning the org creator to the org_owner role.

On invite acceptance: When a user accepts an invite with org_role="org_admin", create an iam_user_roles row linking the user to the org_admin role for that org. The invite's store_role similarly maps to an iam_user_roles row for the appropriate store-level role.

When deny policies are used

Deny policies are for exceptions, not defaults. Examples:

• Temporarily revoking a specific user's access to store.transactions:write (attach a deny policy to a one-off group assigned via a role to that user)
• Compliance lockdowns (deny store.batches:settle across an org during audit)
• Emergency access revocation

---

11. Dafny → Java Compilation

11.1 Compilation Model

Dafny compiles directly to Java. The types defined in Dafny become Java classes — there is no manual mapping step.

dafny build --target:java iam.dfy

Dafny Type	Compiles To	Notes
datatype Effect = Permit | Deny	Java sealed interface + records	Pattern matchable in Java 25
datatype Policy	Java record class	Fields: id, effect, resource, action, conditions
datatype Request	Java record class	Fields: principal, action, resource, context
datatype Response	Java record class	Fields: decision, determiningPolicies, errors, reason
datatype EvaluationError	Java record class	Fields: policyId, message
function checkAccess()	Static Java method	The verified decision function

11.2 What is NOT Compiled from Dafny

The following Java code is hand-written (not generated by Dafny) and therefore not formally verified:

Component	Purpose	Validation Strategy
IamService	Fetches DB state, constructs Request, calls compiled checkAccess()	DRT + unit tests
IamRepository	SQL queries against iam_* tables	Unit tests
IamSeeder	Seeds default roles, groups, policies on org creation	Integration tests
DB ↔ Dafny type conversion	Maps SQL rows to Dafny-compiled Java types	DRT

11.3 Data Flow

JAVA (hand-written)                     DAFNY → JAVA (compiled, verified)
───────────────────                     ────────────────────────────────

Controller:                             IamDecisionEngine (compiled from iam.dfy):
  iamService.checkAccess(                 checkAccess(Request, Set<Policy>) → Response
    authUser,                                │
    "store.products",          ────────►     ├── Step 1: filter to matching policies
    "write"                                  ├── Step 2: if any deny → DENY
  )                                          ├── Step 3: if any permit → ALLOW
        │                                    └── Step 4: else → DENY (default)
        ▼                                        │
  IamService:                                    │
    userId  = resolveUser()                      │
    orgId   = fromContext()                      │
    roles   = iamRepo.getUserRoles()             │
    groups  = iamRepo.getGroupsForRoles()        │
    policies = iamRepo.getPoliciesForGroups()    │
        │                                        │
        ├── construct Request ──────────────────►│
        ├── pass policies ──────────────────────►│
        │                                        │
        │◄────────────── Response ───────────────┘
        │    { decision: Permit|Deny,
        │      determiningPolicies: [...],
        │      errors: [...],
        ▼      reason: "Permitted via store_admin role" }
  return 200 or 403

DRT validates this boundary: generate random (userId, roles, groups, policies, request) tuples, run through both the Dafny reference and the compiled Java, assert identical Response.

---

12. Audit Logging

Every access decision MUST be logged for security monitoring. The log entry includes:

Field	Source	Example
timestamp	System clock	2026-02-16T14:30:00Z
decision	Response.decision	Deny
principal	Request.principal	{userId: "f47ac10b-...", orgId: "org-123"}
action	Request.action	"write"
resource	Request.resource	"store.products"
context	Request.context	{storeId: "store-456"}
determiningPolicies	Response.determiningPolicies	["policy-1"]
errors	Response.errors	[]
reason	Response.reason	"Denied: no matching permit policy"

Log level: INFO for all Deny decisions. DEBUG for Permit decisions. This is implemented in IamService (hand-written Java), not in the Dafny engine.

Important: The ForbiddenException returned to clients MUST NOT include the permission string, policy IDs, or reason. The 403 response body should be a generic "Access denied" message. Detailed information is logged server-side only.

---

References

External

Ref	Link	Relevance
Cedar paper (ICSE 2025)	Cederquist et al., "Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization"	PARC request model, flat permit/deny semantics, skip-on-error, deny-overrides-permit
Cedar language docs	cedar-lang.org	Policy syntax, evaluation semantics
Dafny reference manual	dafny-lang.github.io/dafny	Formal verification language used for checkAccess proofs
Dafny Java compilation	Dafny Compilation to Java	dafny build --target:java mechanics
DRT (differential random testing)	Cedar DRT design	Validation strategy for hand-written wrappers around compiled Dafny

Codebase

File	Description
apps/specifications/dafny/iam/main.dfy	Dafny source — formal spec and proofs (v2, to be written to match this spec)
apps/microservices/merchant-api/.../AuthorizationService.java	Current auth implementation (membership-based, retained as store gate in hybrid model)
apps/microservices/merchant-api/.../IamDecisionEngine.java	Decision engine (v1 modifier-based, to be replaced by compiled Dafny)
apps/microservices/merchant-api/.../IamPermissions.java	Role → permission mappings (to be updated to match Section 9 catalog)
apps/microservices/merchant-api/.../IamRepository.java	Database queries against iam_* tables (to be rewritten for v2 schema)
apps/microservices/merchant-api/.../IamSeeder.java	Seeds default roles, groups, policies (to be rewritten for v2 seeding strategy)
apps/microservices/merchant-api/init.sql	DDL for iam_* tables (to be updated to v2 schema)