include "bufio.m"; include "sexprs.m"; include "spki.m"; sexprs := load Sexprs Sexprs->PATH; Sexp: import sexprs; spki := load SPKI SPKI->PATH; Name, Seqel, Subject, Valid: import spki; verifier := load Verifier Verifier->PATH; Speaksfor: adt { subject: ref Subject; name: ref Name; regarding: ref Sexp; valid: ref Valid; }; init: fn(); verify: fn(seq: list of ref Seqel): (ref Speaksfor, list of ref Seqel, string);
Init must be called before any other operation of the module.
A Speaksfor value represents a claim that a given subject entity speaks for (on behalf of) a given name regarding a set of statements, with validity optionally limited to a given period. That is, when during the agreed time, subject makes a statement that is in the agreed set, it is treated as if name had said it directly. The set of statements is defined by a SPKI `tag' expression, represented as an S-expression. In particular, the (tag (*)) means that subject speaks for name about everything. A claim can be taken as true if supported by acceptable evidence, for instance a collection of signed certificates.
Verify does the actual verification of a sequence seq of SPKI certificates, signatures and operations that makes and supports a claim that an entity speaks for another. It returns a tuple (claim, badel, err). On success, claim refers to a Speaksfor value that summaries the statement verified by the sequence. On failure, claim is nil, badel is a list of sequence elements headed by the first element of seq that failed verification, and err is the reason it failed.
SPKI-VERIFIER(2 ) | Rev: Fri Sep 14 23:38:00 GMT 2007 |