interface # beginning state state user-logged-out begin here subject must not have token "session" state user-logged-in subject must have token "session" and be valid process user-authentication required as input "username" and "passphrase" produces token "session" transition from user-logged-out to user-logged-in via user-authentication transition from user-logged-in to user-logged-out