Testing the Conformance of Implementations of the EAP Protocol and Its Methods to Internet Specifications

Resumo

Generation of tests for checking the conformance of implementations of the Extensible Authentication Protocol (EAP) and its methods to Internet specifications is described. The project is based on the UniTESK technology that allows one to automate the verification of network protocols using their formal models and the extension JavaTesK, which implements the UniTESK technology in Java. The additional use of mutation testing techniques makes it possible to test the stability of a protocol implementation to corrupt messages. This approach proved to be effective in finding a number of critical vulnerabilities and other deviations from the EAP in some implementations.