SPECIFICATION Spec
CONSTANTS
    Users = {u1, u2}
    NumChallenges = 2
    MaxClock = 3
    TTL = 1
    NULL = NULL
INVARIANTS
    TypeOK
    SessionBackedByOwnChallenge
    ChallengeSingleUse
    VerifiedWithinTTL
PROPERTIES
    NoChallengeReplay
    ChallengeBindingImmutable
CHECK_DEADLOCK FALSE