cleanup: stop relying on label injectivity

[TWal]

Builds on #65.

In many proofs, we rely on the injectivity of principal_label, via the pattern

pred = (fun tr pk msg ->
  exists prin. get_sk_label pk == principal_label prin /\
  ... // something that involves `prin`
);

Because of the injectivity of principal_label if we know that get_sk_label pk == principal_label "Alice", then we can use the predicate above with prin == "Alice". This is done in both NSL and ISO-DH.

I now believe that this is more a hack than an actual feature: the labels are used to prove that two keys are distinct (the private key of Alice and the private key of Bob), whereas the goal of labels is initially to prove secrecy.
Proving that two keys are distinct is the role of usages: we already use them to prove that two keys in distinct protocols are distinct (via the "usage tag", e.g. "NSL.PublicKey"), we can also use them to prove that Alice's key is distinct from Bob's key.
This PR uses the "usage data" to store the principal owning the key.

[TWal]

Forgot to mention, this will be useful in #60 where we currently have assumes in the places we needed label injectivity (because we use more fancy labels than just principal_label), and this will also be useful in another future PR that reworks usages.

[qaphla]

The cleanup changes look overall good to me.

The base branch was changed.

[TWal]

(merged, the force-push didn't change the code, you can check that git diff e27024b..0b303e7 is empty)