SPKI-VERIFIER(2)
NAME
verifier: verify − verify sequence of SPKI elements
SYNOPSIS
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);
DESCRIPTION
Verifier checks SPKI proof sequences. This initial implementation provides a single basic operation. Further work will allow (via channels and processes) verification to detect and refresh expired credentials, to support ‘pull’ authentication, for instance.
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.
SOURCE
/appl/lib/spki/verifier.b