Claim Deduction

The verifiable credentials data model is based on a machine comprehensible language called RDF. RDF represents arbitrary semantic knowledge as graphs. Computers can perform automatic deductive reasoning over RDF; given assumptions (represented as an RDF graph) and axioms (represented as logical rules), a computer can infer new conclusions and even prove them to other computers using deductive derivations (proofs).

Every VCDM credential is representable as an RDF graph. So computers can reason about them, deriving new conclusions that weren't explicitly stated by the issuer.

The Dock SDK exposes utilities for primitive deductive reasoning over verified credentials. The Verifier has a choice to perform deduction themself (expensive), or offload that responsibility to the Presenter of the credential[s] by accepting deductive proofs of composite claims.

In RDF, if graph A is true and graph B is true, then the union of those graphs, is also true A∧B->A∪B ¹. Using this property we can combine multiple credentials and reason over their union.

Explicit Ethos

Imagine a signed credential issued by Alice claiming that Joe is a Member.

{
  ...
  "issuer": "Alice",
  "credentialSubject": {
    "id": "Joe",
    "@type": "Member"
  },
  "proof": ...,
  ...
}

The credential does not directly prove that Joe is a Member. Rather, it proves Alice Claims Joe to be a Member.

Not proven:

<Joe> <type> <Member> .

Proven:

<Joe> <type> <Member> <Alice> .

The fourth and final element of the proven quad is used here to indicate the source of the information, Alice. The final element of a quad is its graph name.

A signed credentials are ethos arguments and a credential may be converted to a list of quads (a claimgraph). We call this representation "Explicit Ethos" form. If a credential is verified, then its explicit ethos form is true.

Rule Format

To perform reasoning and to accept proofs, the Verifier must select the list of logical rules wish to accept. Rules (or axioms if you prefer), are modeled as if-then relationships.

const rules = [
  {
    if_all: [],
    then: [],
  },
];

During reasoning, when an if_all pattern is matched, its corresponding then pattern will be implied. In logic terms, each "rule" is the conditional premise of a modus ponens.

{ if_all: [A, B, C], then: [D, E] } means that if (A and B and C) then (D and E).

Rules can contain Bound or Unbound entities. Unbound entities are named variables. Each rule has it's own unique scope, so Unbound entities introduced in the if_all pattern can be used in the then pattern.

{
  if_all: [
    [
      { Bound: alice },
      { Bound: likes },
      { Unbound: 'thing' },
      { Bound: defaultGraph },
    ],
  ],
  then: [
    [
      { Bound: bob },
      { Bound: likes },
      { Unbound: 'thing' },
      { Bound: defaultGraph },
    ],
  ],
}

means

For any ?thing:
  if [alice likes ?thing]
  then [bob likes ?thing]

in other words: ∀ thing: [alice likes thing] -> [bob likes thing]

If an unbound variable appears in the then pattern but does not appear in the if_all pattern the rule is considered invalid and will be rejected by the reasoner.

Bound entities are constants of type RdfTerm. RDF nodes may be one of four things, an IRI, a blank node, a literal, or the default graph. For those familiar with algebraic datatypes:

enum RdfNode {
  Iri(Url),
  Blank(String),
  Literal {
    value: String,
    datatype: Url,
  },
  DefaultGraph,
}

The SDK represents RDF nodes like so:

const alice = { Iri: 'did:sample:alice' };
const literal = {
  Literal: {
    value: '{}',
    datatype: 'http://www.w3.org/1999/02/22-rdf-syntax-ns#JSON',
  }
};
// blank nodes are generally not useful in rule definitions
const blank = { Blank: '_:b0' };
const defaultGraph = { DefaultGraph: true };

Here is an example of a complete rule definition:

{
  if_all: [
    [
      { Unbound: 'food' },
      { Bound { Iri: 'https://example.com/contains' } },
      { Bound: { Iri: 'https://example.com/butter' } },
      { Bound: { DefaultGraph: true } }
    ],
    [
      { Unbound: 'person' },
      { Bound: 'http://xmlns.com/foaf/0.1/name' },
      { Literal: {
        value: 'Bob',
        datatype: 'http://www.w3.org/1999/02/22-rdf-syntax-ns#PlainLiteral',
      } },
      { Bound: { DefaultGraph: true } }
    ],
  ],
  then: [
    [
      { Unbound: 'person' },
      { Bound: { Iri: 'https://example.com/likes' } },
      { Unbound: 'food' },,
      { Bound: { DefaultGraph: true } }
    ]
  ],
}
// all things named "Bob" like all things containing butter

See the claim deduction tutorial for more another example.

Limited Expresiveness

The astute among you may notice the SDK's model for rules does not allow logical negation. This is by design. For one, it keeps the the rule description language from being turing complete so inference time is always bounded. Secondly, RDF choses the Open World Assumption so absence of any particular statement in a credential/claimgraph is not meaningful within RDF semantics.

The rule language is expected to be expressive enough to implement OWL 2 EL but not OWL 1 DL.

Terms

• Verifier: The party that accepts and checks VCDM credential[s].
• Issuer: The party that signed a VCDM credential.
• VCDM: Verifiable Credentials Data Model
• RDF: A model for representing general knowledge in a machine friendly way.
• RDF triple: A single sentence consisting of subject, predicate and object. Each element of the triple is an RDF node.
• RDF quad: A single sentence consisting of subject, predicate, object, graph. Each element of the quad is an RDF term.
• RDF graph: A directed, labeled graph with RDF triples as edges.
• RDF node
• Composite Claim: An rdf triple which was infered, rather than stated explicitly in a credential.
• Explicit Ethos statement: A statement of the form "A claims X." where X is also a statement. Explicit Ethos is encodable in natural human languages as well as in RDF.