Verifiable credentials, the mainstream model for digital identity today, rely largely on the Resource Description Framework (RDF). We argue that while RDF is oriented to 'entities', the world we are willing to represent is essentially based on 'attributes', creating a representation gap. We sketch a formal language and a set-theoretic semantics to illustrate this concept. We eventually show what implications this perspective might bring to our practical implementations of identity frameworks.
The VC data model is based on the Resource Description Framework (RDF) [
While the syntax of a claim is not fully specified, the examples clarify that it is essentially a couple “id” - “attribute” (like in the JSON-LD representation in Figure 1). The data model specifies “the id property expresses an identifier that others are expected to use when expressing statements about the specific thing identified by that identifier” . The data model claims that the “id” property is optional, which would amount to having a credentialSubject including just the attribute. It is, however, legitimate to assume that in this case the attribute is predicated about the bearer of the credential, or the key holder.
Returning to our example, leveraging the formal semantics of RFD [
When building a model, we necessarily only aim at capturing some specific aspects of the reality that are relevant to the problem we want to solve. In our case the problem can be stated as: how can we associate a human being with some attributes in a verifiable way? The answer is simple in case the attribute can be extracted by the physical presence of the person, e.g., ‘eye color’. It is harder when there is no specific relation between the physical presence and the attribute, e.g., ‘citizenship’.
Historically, the basic solution consisted in the possession of some object – e.g., having an armor likely qualified you as being a knight, owning a seal qualifies you as being a bishop – but possession is obviously a weak verifiable mean, since objects can be copied. In this case, the verifiability lies on the complexity and cost of replicating the object (a sort of proof-of-work). However, this approach sufers from the possibility that objects are stolen or voluntarily passed to someone else, and participants need to share some background knowledge on what a specific object is intended to represent. We may introduce ‘speaking objects’, i.e. objects which need not be interpreted, since they carry the information they want to convey: birth certificates (credited to have been introduced by Roman emperor Augustus as wooden diptych with waxed surfaces in 4 AD) provide such an example. Possession of the certificate proves that the bearer holds the attributes annotated in the certificate itself. This example provides an interesting insight, since we can split the problem into two parts: 1) association of the person with some item (in this case, the the wooden tables); 2) association of the item with the attributes (in this case, the birth information engraved in the tables).
We will refer to this intermediate item as the ‘confirmation mean’. In more recent times, this approach evolved using confirmation means for which the association to the person is harder to forge, typically the representation of a biometric feature of the person: a picture of the face can be associated to a person in a reasonably secure way, while the same picture can appear in an identity document, which binds together the picture with the name and additional attributes. In general, the verifiable binding leverages a confirmation mean the person is/have/knows. The same confirmation mean can be used to construct several bindings – e.g., an identity card binds the picture with name/family name, a laissez-passer, a driving license, etc. As it happens, attributes have diferent ‘singling-out power’: a Social Security Number is likely to identify exactly one individual, while a degree only identifies a class of individuals. Singling-out attributes are regularly used for creating chains of bindings to associate a person to their attributes – e.g.: Alice ↔ Alice’s picture via ‘is’ relation; Alice’s picture ↔ Alice’s name via an identity card; Alice’s name ↔ Alice’s degree via a degree certificate (assuming, for the sake of simplicity, that Alice’s name is non-ambiguous). In general, we can assume that documents bind confirmation means to attributes, as well as attributes to attributes. Viceversa, it also makes sense to use more confirmation means to reach the same attribute, e.g., when both a picture and a fingerprint are used to independently establish the name of a person.
In the digital realm, we have the same model. However, we must adopt some diferent form of confirmation means , and a diferent form of documents : • Typical confirmation means in this setting are public keys ( possession of the related private key proves the association), user-ids (knowledge of the related password proves the association), biometric specimens (as far as matching with the real person is feasible). • Documents, which in the physical realm gain their security mainly by engraving the two attributes on a physical substrate, may now assume a variety of forms. However, abstractly they consist of an assertion like < 1, 2 >ℎ- -- where T is a trusted entity1. Technically, the assertion may be made available as a signed file, as a record in a database, on a DLT, etc. Crucially, this assertion needs not be handed over by Alice (the subject).
If we think of confirmation means and singling-out attributes as specific types of attribute, and we think of documents as an implementation of the ‘is bound to’ relation, we eventually come to the simple diagram illustrated in Figure 3.
Once we focus on the aspects of the reality that we want to model, it is straightforward to construct a
formal model. The objective of the formalization is to prove the soundness of the language we want to
1Note that < 1, 2 >ℎ--- is diferent from < 2, 1 >ℎ--- .
use with respect to the underlying model – or at least to fix how identity sentences should be interpreted.
The proposed model has some commonalities with formal approaches to access control like [
An attribute is a couple a = ⟨tag , value⟩ which for syntactic sugar we will type as a = tag : value, where ‘tag ’ belongs to a space of attribute names and ‘value’ belongs to the space of the respective values. Examples of attributes are a1 = name : John; a2 = height : 178 ; a3 = pub-key : 3f3dhc7css8b2323fe.
The tag provides the semantics of the attribute, and it may help the verifier to decide whether to treat it as a confirmation mean or an identifier, how to interpret its format, unit, etc. As a matter of fact, there is need for a standardized ontology of tags to establish a shared semantics. A well-formed formula in our language L is a propositional composition of attributes, i.e.: • an attribute : • a propositional composition of formulas with ∧ ∨ → ¬
We are particularly interested in the subset of these propositional formulas which take the form : → : . Such a formula represents a claim: pub-key : 3f3dhc7css8b2323fe → degree : MscEng is the claim binding attribute ‘pub-key : 3f3dhc7css8b2323fe’ to the attribute ‘degree : MscEng ’. Its intended semantics is: Whoever can prove to be associated with pub key ‘3f3dhc7css8b2323fe’ can also prove to be associated with the attribute ‘degree : MscEng ’. The inference rule is, as usual, by modus ponens. An inference looks like the one in Figure 4.
A model for this calculus would be: M = (I, ), where: • = {1, ....} – intended to represent a set of individuals • : Att → (I) is a function that maps each atomic term of the language : to an element of ℘() (the power set of I) We extend to the entire language : L → U • (¬ A) = (¬ A) (complement in I) • (A ∧ B) = (A) ∩ (A) • (A ∨ B) = (A) ∪ (A) • (A → B) = (¬ A) ∪ (B)
We define |= if () = . Soundness and completeness are derived from propositional logic.
An interesting extension – which we do not explore here – would be construction or a more elaborate calculus with an epistemic flavor, which also accounts for trust relations. Well-formed formulas of this language would be something like: • an attribute : • a claim (1, 2, 3) – meaning: entity described by 1 (likely, a singling out attribute) claims that whichever entity is associated to 2 is also associated to 3. A possible example is c(id : universityOfPadova, pubKey : 3f3dhc7css8b2323fe, degree : MscEng ) • a trust relation (1, 2) – meaning: entity described by 1 (likely, a singling out attribute) trusts entity described by 2 (likely, a singling out attribute). A possible example is t (pubKey : 3f3dhc7css8b2323fe, id : universityOfPadova) • a propositional composition of formulas with ∧ ∨ → ¬ The calculus should be constructed in such a way that we can infer formulas like (, ) ∧ (, 1) ∧ (1, , 1) ∧ (, 1, ) → (, , )
Practically, to verify Alice’s attributes, a relying party needs to perform these steps: • get one or more confirmation means (a picture from a scanner, a public key provided by Alice...) • verify the binding between Alice and a confirmation mean(s) – (via: is/has/knows) • get a set of bindings of which at least one starts from a confirmation mean (from any source) • verify each binding using the respective validation information • follow the chain of bindings starting from a confirmation mean to the desired attributes.
We insist on the fact that the bindings need not come from Alice. The source of the bindings is irrelevant, as long as they are verifiable. We also note that this approach also suits the case where the verifier is interested in performing some inference about some subject outside of an interactive session. In this case, there is no need to get and verify the confirmation means, skipping the first two steps. An additional observation is that we only leverage ‘atomic credentials’, hence there is no need for selective disclosure. Further investigations would be needed to deal with many other important aspects (including unlinkability).