This repository concerns the topic of EPONs security. Model checking is used in this work to derive quantitative results of a MITM attack impact on an energy-efficient mechanism. A number of code files are listed in the repository.