|
Verifying
Group Authentication Protocols by Scyther University
of Agder, Kristiansand, Norway Abstract Scyther is a tool designed to formally analyze
security protocols, their security requirements and potential
vulnerabilities. It is designed under the perfect or unbreakable encryption
assumption, which means that an adversary learns nothing from an encrypted message
unless he knows the decryption key. To our best knowledge, most protocols
analyzed using Scyther are widely used standards
and their complexity are limited. In this paper, we use Scyther
to analyze two complex group authentication protocols [3] and their security
properties. Due to the design goals and limitations of Scyther,
we have only checked a subset of the security properties, which show that the
group authentication protocols provide mutual authentication, implicit key
authentication and they are secure against impersonation attack and passive
adversaries. To achieve this, we have extended the expressing ability of Scyther based on some reasonable assumptions. Keywords: formal verification, group
authentication, Scyther +: Corresponding author: Vladimir Oleshchuk Journal of Wireless Mobile
Networks, Ubiquitous Computing, and Dependable Applications (JoWUA) |