I am reading the paper ‘Town Crier: An Authenticated Data Feed for Smart Contracts’ by Zhang et al (2016), but there is something I just cannot wrap my head around.
In Section 7 and Appendix C, it is stated that three theorems (Authenticity, Gas Sustainability, and Fair Expenditure) are proven following the UC framework. My understanding of this framework is that security of a protocol π is proven by first defining an ideal functionality F, which is a trusted party, and then prove that π realizes the ideal functionality in an environment without this trusted party.
Now, in the proof of theorem 1, they indeed use the formal abstraction for SGX. However, in the proofs of theorem 2 and 3, it seems to me that only the protocols defined in figures 6, 7 and 8 are used and there is no comparison with any ideal functionalities.
So my question is: are these theorems still proven in the UC framework? And if so, what am I missing?