SPECIFICATION Spec
CONSTANTS
  Clients = {c1, c2, atk}
  Attackers = {atk}
  Codes = {k1, k2}
  Tokens = {t1, t2}
  MaxInflight = 2
  NoClient = NoClient
  NoCode = NoCode
INVARIANT TypeOK
INVARIANT SingleUseCodes
INVARIANT TokenBoundToVerifierOwner
INVARIANT RevokedNeverAuthenticates
INVARIANT ExpiredCodesNeverMint
CHECK_DEADLOCK FALSE