Game theory secure probabilistic protocols : Model checking approach

Mr Mahamarakkalage Dileepa Yasas Fernando
Dr Dong Jin Song, Professor, School of Computing

  15 Apr 2019 Monday, 04:00 PM to 05:00 PM

 MR3, COM2-02-26


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.

We observe that there is no automatic verification algorithm to verify BAR-tolerance in probabilistic protocols. Therefore, we introduce probabilistic BAR-model and probabilistic BAR-tolerance property and design verification algorithms. In this thesis proposal, we answer two research questions 1. designing verification algorithms for stopping probabilistic protocols 2. designing verification algorithms for non-terminating probabilistic protocols with rational coalitions and present the preliminary results for third research question of designing scalable verification algorithms for complex protocols.

We design a verification algorithm for first research problem, an approximate verification algorithm for second research problem and plan to implement simulation based verification algorithm for third research problem. We discovered interesting protocol dynamics under probabilistic BAR-model in our case studies. Contrary to the popular belief about the negative impact of Byzantine users, we found improvements to game theory security with the inclusion of Byzantine users.