Authentication builds the trust relationship between communication parties

which is a magnitude guarantee for secure communications.However

existing protocol testing techniques focus on validating the protocol specification.Those techniques can not satisfy the requirements of testing protocol authentication as their lack of the method for describing security properties.Therefore

a protocol security property testing method is proposed for testing protocol authentication.This testing method uses a new formal model-Symbolic Parameterized Goal Extended Finite State Machine (SPG-EFSM) for describing protocols and their security properties.Then

a protocol attack algorithm is designed for testing protocol authentication based on different attack scenarios.Through test experiments on the well-known protocol Woo-lam and TESLA

it is found that the SPG-EFSM based attack algorithm can find several protocol security flaws and has better feasibility and high coverage.