6533b820fe1ef96bd127996d

RESEARCH PRODUCT

Formal Analysis and Model Checking of a Group Authentication Protocol by Scyther

Vladimir A. OleshchukAndreas PrinzHuihui Yang

subject

Model checkingAuthenticationTheoretical computer scienceComputer sciencebusiness.industry020206 networking & telecommunicationsCryptography02 engineering and technologyMutual authenticationCryptographic protocolComputer securitycomputer.software_genreKey authenticationDiscrete logarithmAuthentication protocol0202 electrical engineering electronic engineering information engineering020201 artificial intelligence & image processingbusinesscomputer

description

Scyther [1] is designed to check the security and vulnerabilities of security protocols. In this paper, we use Scyther to analyze two discrete logarithm problem (DLP) based group authentication protocols proposed in [2]. These two protocols are claimed to satisfy several security requirements, but only part of them have been checked because of the properties and limitations of Scyther. Some positive results have been gained and show that the protocols provide mutual authentication and implicit key authentication and are secure against impersonation attack. An important innovation in this paper is that we have extended the expressing ability of Scyther by giving some reasonable assumption during the analysis and security checking.

yearjournalcountryeditionlanguage
2016-02-012016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP)
https://doi.org/10.1109/pdp.2016.27