SPECIFICATION Spec
CONSTANTS
  Agents = {a1, a2}
  Keys = {ka, kt}
  ThiefKeys = {kt}
  BootTokens = {b1, b2}
  ResTokens = {r1}
  AuthTokens = {t1, t2}
  AccTokens = {x1}
  NoKey = NoKey
  NoAgent = NoAgent
  NoRes = NoRes
INVARIANTS
  TypeOK
  SingleUseBootstrap
  KeyBinding
  AuthTracesToGrant
  RevokedGrantNeverServes
  SingleRedemptionPerResourceToken
CHECK_DEADLOCK FALSE