Re: [friam] Formal modeling of systems based on E/CapTP/(Water)Ken/Cap'n Proto ideas

[Oops. Forwarding again, now with the correct subject]

---------- Forwarded message ----------
From: [email protected] <[email protected]>

On 9 Jul 2015, at 17:59, Ben Laurie <[email protected]> wrote:

On 6 July 2015 at 21:59, Mark Miller <[email protected]> wrote:

IANAF -- I am not a formalist. But my co-authors (Sophia and James, cc'ed)
are. Today at PLAS (Programming Languages and Security) Sophia presented

Swapsies on the Internet: First Steps towards Reasoning about Risk and Trust
in an Open World

<http://research.google.com/pubs/pub43808.html>


I started reading it a while back and I have a copy somewhere with
notes on that I can't find right now. sorry.

One thing that struck me is the example doesn't seem to me to address
the problem in the best way, which kinda spoiled the fun for me.

In particular, you make new Purses from existing Purses.

Yes, this is the case.

This (it
seems to me, though perhaps I am missing something) creates an
asymmetry that can be exploited by bad actors.

Can you say how a bad actor would exploit the asymmetry?

We have a proof that the code satisfies the specification - albeit a
hand-developed proof. Also, the proof hinges on the assumption that valid
purses can reliably recommend other objects as valid purses, that it, if a
valid purse executes the method deposit with argument another object and an
amount, and as a result returns true, then the second object is a valid
purse too.

If, instead, Purses
came from Mints, then the two players would be forced to agree on a
Mint which one of them would then have to subvert.

I am not clear whether you mean that the arrow should also be passed a mint
argument?

The escrow agent needs to use (intermediate) escrow purses. The question
arises as to where these escrow purses should come from. In the paper we
have have not explained the rationale for why the escrow agent makes escrow
purses out of the existing purses. We have a better explantation now, and I
will give it now:

 There are the following possibilities:

1) The escrow agent has got them in advance of the transaction
2) The seller and buyer supply the escrow purses to the escrow agent
3) The escrow agent asks the banks of the buyer and the seller for escrow
purses
4) The escrow agent asks the buyer and seller to supply escrow purses.

Now, from the above solutions, 1) would require the escrow agent to know
about all possible purses; but there is no central treated authority. 2)
Would require the buyer and seller to agree with each other before the
transaction; but they do not trust each other. 3) would require the escrow
agent to know about all possible banks; again we have no central trusted
authority. This leaves us with 4), which is what we do in the paper.

I hope this makes some sense?

Sophia

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk