AuthenticationP14V2AuxImpl:
CEDAR
PROGRAM
IMPORTS Convert, Rope, CHNameP2V0Aux
EXPORTS AuthenticationP14V2Aux ~ {
OPEN AuthenticationP14V2, AuthenticationP14V2Aux;
ROPE: TYPE ~ Rope.ROPE;
ExposeSeqWords:
PUBLIC
PROC [arg: SeqWords, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg.body[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeBlock:
PUBLIC
PROC [arg: Block, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..4)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeCredentialsPackage:
PUBLIC
PROC [arg: CredentialsPackage, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "credentials~", ExposeCredentials[arg.credentials, (level+1)], ", "];
res ← Rope.Cat[res, "nonce~", Convert.RopeFromCard[arg.nonce], ", "];
res ← Rope.Cat[res, "recipient~", CHNameP2V0Aux.ExposeThreePartName[arg.recipient, (level+1)], ", "];
res ← Rope.Cat[res, "conversationKey~", ExposeBlock[arg.conversationKey, (level+1)], "]"];
};
ExposeStrongVerifier:
PUBLIC
PROC [arg: StrongVerifier, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "timeStamp~", Convert.RopeFromCard[arg.timeStamp], ", "];
res ← Rope.Cat[res, "ticks~", Convert.RopeFromCard[arg.ticks], "]"];
};
ExposeCredentialsType:
PUBLIC
PROC [arg: CredentialsType, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
simple => res ← "simple";
strong => res ← "strong";
ENDCASE => ERROR
};
ExposeCallProblem:
PUBLIC
PROC [arg: CallProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
tooBusy => res ← "tooBusy";
accessRightsInsufficient => res ← "accessRightsInsufficient";
keysUnavailable => res ← "keysUnavailable";
strongKeyDoesNotExist => res ← "strongKeyDoesNotExist";
simpleKeyDoesNotExist => res ← "simpleKeyDoesNotExist";
strongKeyAlreadyRegistered => res ← "strongKeyAlreadyRegistered";
simpleKeyAlreadyRegistered => res ← "simpleKeyAlreadyRegistered";
domainForNewKeyUnavailable => res ← "domainForNewKeyUnavailable";
domainForNewKeyUnknown => res ← "domainForNewKeyUnknown";
badKey => res ← "badKey";
badName => res ← "badName";
databaseFull => res ← "databaseFull";
other => res ← "other";
ENDCASE => ERROR
};
ExposeStrongCredentials:
PUBLIC
PROC [arg: StrongCredentials, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "conversationKey~", ExposeBlock[arg.conversationKey, (level+1)], ", "];
res ← Rope.Cat[res, "expirationTime~", Convert.RopeFromCard[arg.expirationTime], ", "];
res ← Rope.Cat[res, "initiator~", CHNameP2V0Aux.ExposeThreePartName[arg.initiator, (level+1)], "]"];
};
ExposeWhich:
PUBLIC
PROC [arg: Which, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
notApplicable => res ← "notApplicable";
initiator => res ← "initiator";
recipient => res ← "recipient";
client => res ← "client";
ENDCASE => ERROR
};
ExposeCredentials:
PUBLIC
PROC [arg: Credentials, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "type~", ExposeCredentialsType[arg.type, (level+1)], ", "];
res ← Rope.Cat[res, "value~", ExposeSeqWords[arg.value, (level+1)], "]"];
};
ExposeProblem:
PUBLIC
PROC [arg: Problem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
credentialsInvalid => res ← "credentialsInvalid";
verifierInvalid => res ← "verifierInvalid";
verifierExpired => res ← "verifierExpired";
verifierReused => res ← "verifierReused";
credentialsExpired => res ← "credentialsExpired";
inappropriateCredentials => res ← "inappropriateCredentials";
ENDCASE => ERROR
};