Phoenix Security Analysis
A formal security analysis of the Phoenix transaction model. It defines security models for non-malleability, ledger indistinguishability, balance and note spendability, and proves that Phoenix satisfies each of these properties.