Identity et al (was Re: [E-Lang] Authority -- what is its dual?)

[Jonathan A Rees]

EQ and rights amplification are equivalent (theoretically), but I
think we all like rights amplification better, assuming that you can
get both YES and NO answers out of it in bounded time (I need a name
for this... rights amplification with classification? RAWC).  If you
can implement RAWC in an AYCDISAM (all you can do is send a message)
system, then not only can you simulate passive objects and
non-AYCDISAM systems, you can simulate type *systems*, and prove that
implementations that use ALU's are equivalent to those that use Church
numerals.  So I'm not worried about the actual implementation issues,
if one has RAWC.  The question I'm curious about is how does one best
bootstrap RAWC?  What's the simplest possible actors language?
CBV lambda-calculus + state + concurrency?

(Remember that Will Clinger got out of the Actors business because it
was too complicated for his taste.  On graduating ("Foundations of
Actors Semantics", MIT PhD 1981) he switched to Scheme and never
looked back.)

   From: "Mark S. Miller" <markm@caplet.com>
   >[JAR] I'm worried about the necessity of a having a private communication
   >path (capability) from object to verifier.  Digital signatures don't
   >have this property, which makes me worry that the approach is flawed,
   >or at least not robust to partitions.

   This doesn't apply to Act-1 or Joule, ...

I was a bit confused here, and I want to go over this again because
it's an important point.  Here is my paraphrase of Dean's explanation
of rights amplification a la Joule (which so far is the only way I've
heard of to do it assuming AYCDISAM):

Part 1. Client's point of view: If Alice wants to verify that Cereal
has the Kellogg brand, she sends a message to Kellogg.  A while later,
she may get a message carrying Kellogg-Cereal, or she may not.  If she
gets Kellogg-Cereal, then she knows it has the Kellogg brand, and can
proceed accordingly.  If she waits a while (bounded by a time limit
that Dean tells us) and gets nothing, then Cereal doesn't appear to
hold something with the Kellogg brand.  (We all know how to use
capabilities and facets to ensure appropriate communication privacy,
so I've omitted those details.)

Alice is careful not to lend too many computing resources to Cereal in
case Cereal is an unresponsive service denier.

Part 2. Brand's point of view: Having heard Alice's question, Kellogg
sends a message to Cereal that says in effect "Please find a
Kellogg-Cereal, perhaps yourself, and tell it to contact me on a
channel (facet) that it knows and you may not."  The Kellogg-Cereal,
if there is one, sends Kellogg a direct pointer to itself so that it
can be contacted directly, which is necessary since Cereal itself
might present a haze of interference.  If such a message comes into
Kellogg, Kellogg forwards it to Alice.  No such message will come
along if Cereal doesn't have the Kellogg brand.

When I said that a "private communication path (capability)" is
needed, I was referring to the "channel that only Kellogg-branded
Cereals know about".  Since writing this it occurred to me that the
capability graph needn't be related to the potential-communication
graph; it may be that Kellogg-Cereal and Kellogg have no way to talk
to one another most of the time (in fact it's essential that it be
possible to use Kellogg-Cereal on a laptop not connected to Kellogg),
but at the point that Alice asks her Kelloggness question, she can
talk to both, so there is certainly at that time a way for the message
to get through from Kellogg-Cereal to Kellogg -- at worst, Alice can
route it.

This routability may also be the key to bounding the time required to
establish a NO answer.  The bound could be in terms of bandwidth and
latencies between Alice, Kellogg, Cereal, and Kellogg-Cereal.  (I
still find this disgusting and probably theoretically intractable, but
we can address those issues later.)

That said:
Because of the Cereal-to-Kellogg-Cereal coercion, the above isn't the RAWC
that I was hoping for, which in my mind would be able to tell you
something about Cereal, not just about Kellogg-Cereal.  Perhaps it's
good enough for all practical purposes, but I don't see why I
shouldn't want true object classification.  How about
this scenario:
  1. Bob gives Cereal to Alice.
  2. Alice disconnects from network, including Bob and Kellogg.
  3. Alice verifies, while disconnected, that Cereal is indeed a
     Kellogg-Cereal, and proceeds to use it.
(Variant: Alice and Kellogg are already disconnected when Bob gives
Cereal to Alice.)
In the real world, this is easily done using digitally signed messages
-- Alice just needs to know Kellogg's public key.  But I don't see
how to do translate this scenario into AYCDISAM.

Idle aside: The timeout reminds me of "retracts" in denotational
semantics; a retract is a function that is undefined (hangs) for all
inputs other than those belonging to some type specific to that
retract.

I didn't know that transparent forwarders were transparent even to EQ.
I should learn how this works; haven't been following this.  (The URL
was sent recently so don't worry, I can find it.)

Mark, I hope that E can ultimately make rights amplification work in a
distributed manner, using brand-specific encryption keys?  E.g., could
sealed objects be selfless?  I know this is low priority, and that's
fine, but by my thinking (today) it'll be very important eventually.
I hope there's no principled reason that you think a brand's
population of sealed objects all have to reside in the same vat.

-JAR (i.e. Jonathan Rees, using "JAR" to distinguish himself from Jonathan)