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