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: Tue Mar 31 02:42:39 GMT 2015 |