Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis
Matthias Cosler
Fair exchange protocols, also known as non-repudiation protocols, are a special class of protocols that should ensure a kind of fairness. A real-world example of this problem may be a hostage exchange as portrayed in many movies. The goal is to ensure that no party can gain an advantage by fooling the other party, e.g., by denying the receiving, canceling the exchange during the process, or by waiting too long. An application for these protocols are smart contracts, also known as the contract-signing problem. This class of protocols can be modeled and verified using game-playing techniques and Alternating Time Temporal Logic (ATL resp. ATL*), an extension of Computation Tree Logic (CTL). ATL extends CTL with the ability to quantify over strategies and capabilities of players. Designing correct protocols is hard for humans as various security issues in protocols such as the Needham-Schroeder-Protocol or Kerberos have shown. Instead of relying on the skills of humans while designing protocols, we aim at synthesizing such protocols directly from ATL* specifications. In this thesis, we present a reduction from ATL* synthesis to (Hyper-)LTL synthesis. Our technique ought to be easy to implement, as general as possible and benefit from the optimizations of existing LTL synthesis implementations, such as BoSy(Hyper). The main idea in this reduction is labeling witnesses of satisfaction for path formulas into the computation tree and using these to encode the ATL path quantification..
Bachelor Thesis.