<> <> <> <> <> <<>> DIRECTORY IO USING [STREAM], Rope USING [ROPE], UserCredentials USING [defaultOptions, LoginOptions, State]; UserCredentialsBackdoor: CEDAR DEFINITIONS = BEGIN <<>> ROPE: TYPE ~ Rope.ROPE; STREAM: TYPE ~ IO.STREAM; GuestProcsRec: TYPE = RECORD [ IsGuestProcess: PROC [] RETURNS [isGuest: BOOL], GetState: PROC RETURNS [UserCredentials.State], ChangeState: PROC [new: UserCredentials.State] RETURNS [old: UserCredentials.State], Login: PROC [ startInteraction: PROC RETURNS [in, out: STREAM], endInteraction: PROC [in, out: STREAM], options: UserCredentials.LoginOptions _ UserCredentials.defaultOptions ], Get: PROC RETURNS [name, password: ROPE] ]; RegisterGuestProcs: PROC [newProcs: REF GuestProcsRec]; END.