Sketching a formal model for “verifiable identity”

This is a sort of a formal exercise and can be skipped with no prejudice. It aims at sketching a formal model (syntax and semantic) capturing the concepts described here.

Syntax

We introduce a simplified syntax for exemplification. The syntax is completely arbitrary, but can easily be mapped to existing JSON, XML, ASN1… notations and appropriately extended.

The alphabet includes:

A term for an attribute is a concatenation: ti:vj (like, for example, eyeColour:brown). The set of terms for attributes, is then

A formula in our language is defined as b(ti:vj,th:vk) where ti:vj, th:vk are terms for attributes. For example, b(id:did123, eyeColour:brown) is the formula to say “attribtue id:did123 is bound to attribute eyeColour:brown” or, said differently, “whoever can prove to be associated with attribute id:did123 can also prove to be associated with attribute eyeColour:brown”

The language is defined as the set of formulae, i.e.

The natural calculus for this language is defined as follows. Given F ⊆ Lan,

Where F ⊢b(ti:vj,th:vk) reads “the set F demonstrates the formula b(ti:vj,th:vk)”.

Semantics

A formula b(ti:vj,th:vk) is intended to mean: “whoever can prove to be associated with attribute ti:vj can also prove to be associated with attribute th:vk”. We capture this in the semantics.

Let M = (I, A, σ) be a model for our language, where

For any formula b(ti:vj,th:vk)∈ Lan we define

Which reads: the model M satisfies the binding b(ti:vj,th:vk) if and only if the interpretation of the first attribute is a subset of the interpretation of the second attribute.

A set of formulae F ⊆ Lan is said to be coherent if there exists a model which satisfies all formulae in F. A set of formulae F ⊆ Lan is said to be incoherent if there is no such model.

Given F a coherent subset of Lan we define M ⊨ F (read: M satisfies F) as

Eventually, we define F ⊨ f (read: F satisfies f) if any model for F is also a model for f: