docs/proof": Strengthen authenticity property.

The current formalization of the authentication protocol involves
both the dialer and acceptor taking in the expected public key of the
other end as an input, and then verifying that the blessings received
during the protocol are for these public keys. This check is more of an
"authorization" check and is not strictly needed for proving the
authenticity property.

This CL gets rid of the "expected public key" check from the acceptor
thus allowing the acceptor to accept a connection from any dialer ---
this is indeed the case in practice. (The dialer still retains the
expected public key check, more on this below.)

Now we change the authenticity property to say that if the acceptor
accepts a connection with the dialer's public key then the dialer must
have accepted a connection with the acceptor's public key, and vice
versa. Note that we allow the acceptor to accept a connection with a
public key different from the dialer (e.g., an attacker may open his own
connection to the acceptor).

The dialer still needs to perform the expected public key check in order
to achieve the dialer privacy goal. Essentially, if the dialer does not
employ a peer authorization check then it may reveal its blessings to
the attacker.

Change-Id: I05ba88813996ab630dcc80a3a3696020ea9a4607
2 files changed
tree: b409a574857390916f5ed02a214796c9ed8d33ef
  1. concepts/
  2. contributing/
  3. designdocs/
  4. images/
  5. proofs/
  6. tools/
  7. tutorials/
  8. .gitignore
  9. AUTHORS
  10. CONTRIBUTING.md
  11. CONTRIBUTORS
  12. glossary.md
  13. installation.md
  14. LICENSE
  15. PATENTS
  16. README.md
  17. tos.md
  18. VERSION
README.md

Welcome to the Vanadium github repositories! Vanadium is an open source framework created by engineers at Google that is intended to make it much easier to develop secure, distributed applications that can run anywhere and everywhere. It provides:

  • a complete security model, based on public-key cryptography, that supports fine grained permissioning and delegation. The combination of traditional ACLs and “blessings with caveats” supports a broad set of practical requirements.
  • symmetrically authenticated and encrypted RPC. The RPC model is bi-directional, supports streaming and can be run through proxies. The result is a secure communications framework that can be used for large scale data-centre applications as well as for enterprise or consumer applications that need to navigate NAT boundaries.
  • a self-describing encoding format that is both performant and designed to support a broad range of programming language semantics (today we have support for go, java and javascript).
  • a global federated naming service that offers the convenience of urls but allows for federation and multilevel resolution. The ‘programming model’ consists of nothing more than invoking methods on names, subject to security constraints.
  • the ability to use multiple global and/or local identity providers (e.g. Google, Facebook, Microsoft Exchange, pam etc). We currently provide an oauth2 based implementation but the others mentioned would work just as well.
  • a storage service, Syncbase, that can be run on all devices, small or large, and offers synchronized peer-to-peer storage. Syncbase offers:
    • a structured store that can be queried using a sql-like language,
    • a blob store that synchronized content across all multiple devices,
    • the ability to group data into ‘synchronization groups’ to control which devices are synchronized,
    • fine grained access control,
    • peer-to-peer synchronization and conflict resolution,
    • offline operation is inherently supported.

We believe that the APIs should be well designed and stable and have taken pains to separate our APIs (v.io/v23) from all of our code that implements them. We provide a backwards compatibility guarantee for the APIs and have carried out usability testing on the APIs themselves.