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: