Game theory secure probabilistic protocols: A model checking approach
COM1 Level 3
MR1, COM1-03-19
Abstract:
Protocols play an important role in machine interactions as well as human interactions. Malfunctioning protocols can result in immense financial impact, or impact on human life. It is important to verify that protocols are free of malfunctions and achieve its design goals. The verification is computationally challenging in general, due to the complexity of protocols.
Conventional verification methods verify correct execution by assuming honest behaviour or adversarial behaviour. A protocol verified by the above methods can still operate incorrectly due to selfish or arbitrarily deviating users and is more challenging to verify due to additional complexity . A protocol is called game theory secure when selfish users follow it correctly. Existing work verify, model such protocols as Byzantine, Altruistic, Rational model (BAR in short) and model game theory security as BAR-tolerance.
There is no automatic verification algorithm to verify BAR-tolerance in probabilistic protocols. Therefore, probabilistic BAR-model and probabilistic BAR-tolerance property are introduced and verification algorithms are designed. In this thesis, three research questions are answered
1. designing verification algorithms for stopping probabilistic protocols 2. designing verification algorithms for non-terminating probabilistic protocols with rational coalitions
3. designing scalable verification algorithms for complex protocols.
A verification algorithm is designed for the first research problem, an approximate verification algorithm is designed for the second research problem and a simulation-based verification algorithm is implemented for the third research problem. Finally, the verification algorithms are integrated in PAT model checking tool.
I discovered interesting protocol dynamics under probabilistic BAR-model in my case studies. Contrary to the popular belief about the negative impact of Byzantine users, I found improvements to game theory security with the inclusion of Byzantine users.