Security protocols are widely used in open modern networks to ensure safe communications. It is now recognized that formal analysis can provide the level of assurance required by both developers and users of the protocols. Unfortunately it is generally undecidable to certify whether a protocol is safe or not. However the automatic verification of security protocols can be attempted using abstraction-based approximation. For this purpose, tree automata approximations were introduced by Genet and Klay in 2000. In this paper, we propose an extension of their techniques making the approach efficiently automatic. Our contribution has been implementing in the TA4SP tool with a high level specification language as input format, providing positive practical results on industrial security protocols.