Dynamic Labelling

[qaphla]

Starting this as an umbrella issue for figuring out how we want to handle dynamic labelling.

As of now, there are two main use cases that we have for dynamic labelling.

1. In some cases, while there is a fixed set of participants who know some value, that set is not known to the creator of the value at creation time. To handle this, we could use something like a "placeholder" label, which refers to a single, as yet unknown, participant.
2. In group protocols, for example, when a group is dynamically adjusted, some secret may need to be revealed to the new group member. This requires a more general form of dynamic labels, as we generally do not statically know how large a group may end up being.

Other ideas of use cases that differ in technical needs would be helpful to mention here as they come up.

Our past discussion led to one main idea for handling dynamic labels --- to introduce a form of "label indirection", where we would, on creation of a new value, give it a label identifier, rather than a concrete label, and the link between that identifier and an actual label would be on the trace --- first at the nonce creation, and then it could be altered by future trace entries. It is not currently clear exactly what those trace entries should look like --- perhaps they could be of the form "reveal label identifier X to party Y", or something more precise (e.g., "update identifier X to refer to label Y", with some constraint to ensure that values cannot suddenly become more secret). We also discussed the idea of a "final" flag on label identifiers, indicating that they can no longer be updated, which could be set either at creation time or at some later point.

A key question is what problems it causes to not be able to determine information about a label independent of the trace. My feeling is that since we should only ever be comparing labels via can_flow, which requires a trace anyway, this is fine, but there may be edge cases I'm missing.

[TWal]

A few thoughts about this:

A while ago I tried to remove labels from the bytes constuctor: the label of a random bytestring would be RandLabelAt i, acting like an indirection to look for the label somewhere in the trace. https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/fccc0b1bcfa04bcf8c0f2f6a1abd2b6268fc628a/src/DY.Core.Label.Type.fst#L42 Now, it is impossible to say that get_label sk == principal_label alice because get_label sk is not a State label but a RandLabelAt …. Instead we can say that equivalent tr (get_label sk) (principal_label alice), i.e. labels can flow in both directions.

Unfortunately, it doesn't work with a proof style we use, e.g. in the public-key encryption predicate of NSL: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/fccc0b1bcfa04bcf8c0f2f6a1abd2b6268fc628a/src/DY.Example.NSL.Protocol.Total.Proof.fst#L25-L47

In exists prin. get_sk_label pk = principal_label prin /\ (... some properties involving prin ...), we effectively invert the sk_label of pk to obtain a principal. Thanks to the injectivity of principal_label, if we know that get_sk_label pk = principal_label alice, we know that the only possible prin is alice, and we obtain the next properties with alice.

Unfortunately, it doesn't work when we replace label equality with equivalence, because we loose the injectivity property: for example, we may have equivalent tr (principal_label "Alice") (principal_label "Bob"), when both Alice and Bob are corrupt.

It may work with a different version of equivalent: right now, is_equivalent tr l1 l2 means

  can_flow tr l1 l2 /\
  can_flow tr l2 l1

which is equivalent to

 forall tr_extended. tr <$ tr_extended ==>
    (is_corrupt tr_extended l1 <==> is_corrupt tr_extended l2)

We could work with a stronger version without the tr argument:

let equivalent l1 l2 =
 forall tr.
    (is_corrupt tr l1 <==> is_corrupt tr l2)

and here we would indeed have the injectivity property equivalent (principal_label prin1) (principal_label prin2) ==> prin1 == prin2.