"Sure, but one can formalize the properties of Bitcoin, and could prove that it indeed meets those properties." This seems a bit backwards. Rather than formal

"Sure, but one can formalize the properties of Bitcoin, and could prove that it indeed meets those properties." This seems a bit backwards. Rather than formalizing the properties of Bitcoin, it seems that we should be formalizing the goal of Bitcoin i.e. the properties we want, and then prove that Bitcoin satisfies those properties (if it does actually satisfy them). I think that such a formalization would require a formalization of the entire Bitcoin concept of money, which would probably be beneficial in and of itself. "If we give up having a central authority and verified identities, we necessitate some measure of "majority of power" in the system" I think that really depends on your notion of money. If you are like me, you believe that money has value because of its utility: fiat currencies have utility that is defined by a legal system (taxes, debt law, torts, etc.), but one could imagine something else. Suppose, for example, that you had a digital cash system in which the money was redeemable for CPU time in a secure outsourcing system; this could potentially be decentralized. Controlling more computing resources would not give an attacker greater power over the network, but would allow a party to receive more payments (because they are basically selling access to their CPU). It is of course possible that such a system could not be securely realized for technical reasons. "One of these properties is "network is controlled by the majority of computing power"." This is not a very precise definition, at least not in the cryptographic sense. What is the formal definition of computing power here -- what is the computation model? It would be very hard to prove that a system has this property in a rigorous way. On the other hand, in the system I described above, you could formalize the measure of how much work a node did (and how much payment was received) by using circuit families as the computation model and the number of gates evaluated as the measure of work. This sort of abstraction would allow a rigorous proof of various properties of the protocol; e.g. maybe you want to show that the payment a party receives will be some proportion of the number of gates the party evaluates. "As you later touch upon, once you get rid of identities, a single attacker can create an unlimited number of parties." Not unlimited; the attacker's ability to enter parties into the system is bounded by the computing power of the attacker. If the attacker can only scale their computation by some polynomial in the parameters of the system, the attacker can only enter some polynomial number of parties. If the protocol is secure as long as there is one honest party, the attacker would not be able to win even under such a scenario. "I think general MPC has only been proved secure if a majority of parties are honest." It is not really that simple. For example: http://eprint.iacr.org/2012/441.pdf http://eprint.iacr.org/2012/441.pdf There is a protocol that is secure even if only one party is honest. The problem here is that "secure" does not have a single meaning in MPC. There are various adversary models: an adversary might only be able to choose which parties to corrupt before the protocol runs, or might be able to corrupt parties while the protocol is running; he might be allowed to adapt the attack between the computation rounds and the output round, as in that paper; he might be allowed to compose protocols together in arbitrary ways; etc. Some protocols require a setup phase or an authority, some are standalone (as in the paper), some require a broadcast channel, and so forth.