w3c / N3

W3C's Notation 3 (N3) Community Group
48 stars 18 forks source link

Pointing into nodes in surfaces #206

Open bblfish opened 1 year ago

bblfish commented 1 year ago

The Verifiable Credentials Data Model has an interesting diagram of how they see the structure of a Credential, which I reproduce below from the Figure 6 of §3.2 Credentials

Credentials Graph image from spec

As argued in issue 1248 of the VC repo the JsonLD does not seem to map to that data structure, where the colored surfaces are mapped to N3 {...} contexts. In issue 1248 I tried to map as closely as I could to N3, but came across these two problems for which I was not sure what the best encoding would be:

  1. the :credentialSubjectrelation points from the Credential123 node on the pink surface into the yellow Claim surface to its right. But it does not point at the claim, i.e, at the surface border, but into a node in the claim, namely the node named :Pat.
  2. We also have an arrow from the top Pink Credential Graph surface - starting here from the borer of the surface - into the bottom Green Credential Proof Surface node :Signature456 node.

I don't think the lower claim must be on its own surface. And I am unsure if there is a need to point to the node on the surface in those two cases. Still, I wonder if and how N3 could represent it.

bblfish commented 1 year ago

Of course, we do this with hash URLs such as <https://bblfish.net/people/henry/card#me>, which point to a node in a graph. But can that be done for anonymous graphs?

TallTed commented 1 year ago

I think this is not an N3 issue, but a VCDM issue.

I think you're correct, that the Credential Graph should point to the Credential Proof Graph; i.e., that the proof arrow should be between the large enclosures, each of which should have its own identifier, whether that be explicit (URI) or implicit (bnode).

I think there are some other issues with this diagram which stem from its original creation, rather early in the VCDM process, combined with later efforts to simplify it (for instance, to include just one claim), which unfortunately removed and/or distorted elements which may have been more correct in the earlier version(s), or may never have been quite correct.

bblfish commented 1 year ago

I think this is not an N3 issue, but a VCDM issue.

It is an N3 question for the rdf proposed in §2 and §3 of vcdm issue 1248, but not for §4. It is more a question for the n3 group as an issue for it. Also, this is an important use case for reasoning with n3 :-)

I think you're correct, that the Credential Graph should point to the Credential Proof Graph; i.e., that the proof arrow should be between the large enclosures, each of which should have its own identifier, whether that be explicit (URI) or implicit (bnode).

I have the following argument about how one can go logically from one to the other.

In §2 N3 corresponding to the VC Credentials diagram

I proposed representing the N3 as shown in the diagram above. There, we have the link into the yellow surface onto a node, which I thought could be represented as

<1872> 
    cred:credentialSubject <did:example:ebfeb1f712ebc6f1c276e12ec21> ;
    cred:claim { 
    <did:example:ebfeb1f712ebc6f1c276e12ec21>
         schema:alumniOf [ id <did:example:c276e12ec21ebfeb1f712ebc6f1> 
               schema:name "Exemple d'Université"@fr ,   "Example University"@en 
         ] 
   }

and the second is the link from the top surface into the lower one

{ ... }  sec:proofObject _:gn;
          sec:proof {
                _:gn  a sec:RsaSignature2018 ;
              ...
         }

In both cases, there needs to be a link to the context (N3 spec calls them Graph Terms I just noticed) with the cred:claim and sec:proof relations, and a link to the object within those graphs cred:credentialSubject and sec:proofObject. I think it is inevitable that one has both.

On the web, we can get away with only one relation to an object <...card#i> because the dereferencing operation of fetching the data then gives us the graph, so it need not be written out. But as VCs are signed, all the data has to be present.

In §3 "Slight Simplification of N3 translation of Diagram"

I simplify that by arguing that all the other surfaces are actually on the green surface, that is, we have, in the says logic

\text{ UniKey } \text{ says } \text{ Uni } \text{ says } \text{UniAlumni}(\text{Pat}, \text{Uni})

But the outer green surface is a positive one -- asserting facts -- so we can avoid the green context. It follows then that the lower green surface triples can be thought to be in the default graph. (Here, we keep the yellow claim surface, as above.) I think there is very likely absolutely no danger in doing this, especially as all the attributes are attached to a blank node, so merging with other true graphs should not mess up the proof.

Credential Proof in default graph

In this model, we keep the yellow surface separate, and so we still need both a pointer to the surface and a pointer into the surface. In banana-rdf, Alexandre Bertails named these PointedGraphs.

In untyped N3, perhaps these could be written as a pair of a pointer and a graph

<1872> cred:credentialSubject ( 
        <did:example:ebfeb1f712ebc6f1c276e12ec21>
        {  <did:example:ebfeb1f712ebc6f1c276e12ec21>
              schema:alumniOf [ id <did:example:c276e12ec21ebfeb1f712ebc6f1> 
                  schema:name "Exemple d'Université"@fr ,   "Example University"@en 
              ]
        }
  )

Perhaps that is also available to JsonLD.

This model is, I am sure, good.

Also, you should be able to merge this graph with other graphs and never get confused about anything, as your proof object is a blank node.

In §4 the proposed intended model

In §4, we remove the yellow surface from the previous proposal, so here, it is no longer clear what the claim and the metadata about the issuer is.

CredShouldBe

But that may also be okay because of the monadic-like says rule, which goes

\forall s: \text{Agent}, p: \text{Prop} . s \text{ says } s \text{ says } p \to s \text{ says } p

I think this, together with the rule that

\forall a,b: \text{Agent}, p: \text{Prop}. a \text{ speaksFor } b \to a \text{ says } p \to b \text{ says } p 

and the following

k \text{ says } s1 \land s2 \iff k \text { says } s1 \land k \text{ says } s2

can help us see that the these follows. That is because the structure of the previous digram was of the form

U_k \text{ says } (p  \land (U \text{ says } q)

Where $U_k$ is the university key, $U$ is the university and $p$ and $q$ are arbitrary propositions, and since we assume that $U_k \text{ speaksFor } U$ we have it that it follows that

U \text{ says } (p  \land (U \text{ says } q))

which means that

(U \text{ says } p)  \land (U \text{ says } (U \text{ says } q))

so that we can simplify the second half to

(U \text{ says } p)  \land (U \text{ says } q)

which is equivalent to

  U \text{ says } (p  \land q) 

That is, the internal yellow surface can disappear. One can also go the other way, so it does not seem to bring that much. But here, a more careful logical analysis would help.

Why the current model is wrong

Here I am considering this one that I got by jsonld conversion

CredFromJsonLd

But consider merging this graph with another true graph. This could quickly render the signature meaningless. Take for example, the true graph

<did:example:ebfeb1f712ebc6f1c276e12ec21> foaf:name "Pay Hayes";
      foaf:publications <https://scholar.google.com/citations?sortby=pubdate&hl=en&user=VTNr4NMAAAAJ&view_op=list_works> .

If we merged that to the representation where only the signature is a surface, the new graph would consist of the intact green surface, the other data and those three triples on the same default surface. I.e. we have the following graph, and it would no longer be possible to know what was signed. Crential Merged

Compare this to the much more correct merging of the simplified model of §4 with the true Pat Hayes graph.

Cred graph of §4 union a true graph about Pat

Here we can still verify the Credential Graph using the Proof object, and if we still believe it, then we can merge the content of the pink surface and the rest without problem.

That indicates clearly that the current model is not workable.

I think you're correct, that the Credential Graph should point to the Credential Proof Graph; i.e., that the proof arrow should be between the large enclosures, each of which should have its own identifier, whether that be explicit (URI) or implicit (bnode).

So, I think we need only the proof object; we don't need a proof surface.

I think there are some other issues with this diagram which stem from its original creation, rather early in the VCDM process, combined with later efforts to simplify it (for instance, to include just one claim), which unfortunately removed and/or distorted elements which may have been more correct in the earlier version(s), or may never have been quite correct.

So it looks to me like the diagram of §2 entails the simpler ones (§3 and §4) after setting the green surface to be the default graph. But it certainly should not entail the one that it is currently found by jsonld translation to n3, as explained in §1 of issue 1248.