[e-lang] Proofs of holding a capability (was: chat with kpreid)

[David-Sarah Hopwood]

Mark Miller wrote:
[...]
> 8:11 PM Nonce's grant access. SwissNumbers grant persistent access.
> SwissHashes grant ability to claim sameness, for example, for a
> capabilities-as-keys comparison based service on VatB.
>  kpreid: SwissNumbers don't grant persistent access in general.
>   The 3-vat protocol uses swiss numbers, doesn't it?
>  me: This may be a bad design -- the swissHash may be granting more
> access than it should. But that's what I was thinking.
> 8:12 PM kpreid: Well, swissnumber says you have access to the object.
> And you can compute the shash from the snum. So the snum shouldn't be
> authority-to-claim-to-be.
>  me: No. Not since we switched to the nonce/table-based protocol.
>  kpreid: the shash, I meant
>  me: Yes, but only for Far3Desc. Promise3Desc doesn't carry a shash.
> 8:13 PM kpreid: Well, but that's wrong.
>  me: Why?
>  kpreid: I shouldn't be able to spoof an identity by knowing the hash...
>   by knowing the snum (which implies knowing the shash) I mean
[...]

We're probably missing some context, but the issue here seems to be
some prover, peggy, needs to be able to demonstrate to a verifier,
victor, that peggy holds a capability C, such that:

 - if victor already holds C, or comes to hold C, then it will recognize
   which of the capabilities it holds is the same as C, and know that
   peggy also holds it (and that C is associated with a particular proof);

 - if victor does not hold C then it obtains neither C, nor the ability
   to give a proof of holding C that will be accepted by other verifiers.

Ideally we want a noninteractive proof that does not require public key
cryptography, other than that required to set up a secure session.

Note that in the case where peggy and victor are vats communicating by
CapTP, there will already be a shared session secret, S_session. If S is
derived by a suitable Key Derivation Function from something like a TLS
master secret, then it is determined by random per-session contributions
from peggy and victor such that neither of them alone can force its value
to be the same as for any previous session between any pair of vats. The
ability to obtain a session secret would also be required by WormholeOp.


Unoptimized protocol to demonstrate feasibility:

Let the proof that peggy holds C in a given session be
P_{C,session} = H(S_session, SwissNum_C), where H is a collision-resistant,
second preimage-resistant, and oneway hash, and SwissNum_C is a globally
unique unguessable identifier for C.

To verify this proof, victor calculates
P_{X,session} = H(S_session, Swissnum_X) for all capabilities X that
it holds. If P_{X,session} = P_{C,session} for some X, then X is the
same as C.


Informal security analysis:

If an attacker can find P_{X,session} = P_{Y,session} for any session
and capabilities X and Y that are not the same, then either
SwissNum_X = SwissNum_Y (contradicting global uniqueness of Swiss numbers)
or the attacker has broken collision resistance of H.

If an attacker can obtain significant information about SwissNum_X
from H(S_session, SwissNum_X), then it has broken onewayness of H.
If given any P_{Y,session} it can generate a new SwissNum_Z such that
a proof of holding Y will also be valid for Z, then it has broken
second preimage resistance of H.

If victor can force S_session' with another verifier to be the same
as S_session with peggy, then it has broken the assumption stated
earlier about the session key of the secure transport protocol.
Without this ability it cannot replay proofs that will be accepted by
another verifier (or, assuming onewayness and second preimage resistance
of H, otherwise construct new valid proofs from old proofs).


Optimization:

The protocol as described above is inefficient because it requires
victor to calculate *per-session* hashes P_{X,session} for all of the
capabilities it holds.

This can be improved by associating each capability X with a "hint"
SwissHint_X (globally, not per-session). SwissHints need not be unique
nor high-entropy, although they should not give away information that
would aid in guessing their SwissNum. Each vat constructs a hash table
mapping SwissHints to the corresponding SwissNums for all the
capabilities it holds.

A proof of holding C becomes a pair (SwissHint_C, H(S_session, SwissNum_C)).
The verifier looks up SwissHint_C in the hash table, which tells it
the SwissNum(s) that *could* match, and then checks them as in the
original protocol. If SwissHint_C is not unique, then the verifier
just checks all potential matches.

Note that unlike proofs in the unoptimized protocol, a proof now does
give away transferrable information about the identity of the capability
it is associated with. It just isn't sufficient information to construct
a proof that will be accepted by an honest verifier. Even a dishonest
verifier (i.e. one that is prepared to accept any implication of the
proof without necessarily following the verification protocol) will
at most have reason to infer that the prover heard some proof that
someone holds the capability, not that it holds the capability itself.


> 8:40 PM OK, answer this question alone: Given that VatB knows Carol,
> how does VatA securely identify the existing B-ref-to-Carol in talking
> to VatB, in ignorance of B's knowledge of Carol?
> 8:41 PM me: The present answer is the swissHash. "SwissHashes grant
> ability to claim sameness"
> 8:42 PM kpreid: OK, by "claim sameness" you mean something unobvious.
>   You mean "ability to claim I have the ref you have" apparently
>  me: yes
> 8:43 PM kpreid: It sounds like "ability to claim my ref is the same as
> some other ref"
>  me: Again, this may be a bad design. I am worried about it.
>   yes.
>  kpreid: Please find better terminology
>  me: Please help me do so ;)

This is the "proof of holding" described above. I hope this is better
and more precise terminology.

-- 
David-Sarah Hopwood  ⚥  http://davidsarah.livejournal.com