Wireless networks are more vulnerable to cyberattacks than cable networks.Compared with the misuse intrusion detection techniques based on patt matching,the techniques based on model checking (MC) have a series of comparative advantages.However,the temporal logics employed in the existing latter techniques cannot express conveniently the complex attacks with synchronization phenomenon.To address this problem,we formalize a novel temporal logic language called attack signature description language (ASDL).On the basis of it,we put forward an ASDL model checking algorithm.Furthermore,we use ASDL programs,which can be considered as temporal logic formulas,to describe attack signatures,and employ other ASDL programs to create an audit log.As a result,the ASDL model checking algorithm can be presented for automatically verifying whether or not the latter programs satisfy the formulas,that is,whether or not the audit log coincides with the attack signatures.Thus,an intrusion detection algorithm based on ASDL is obtained.The case studies and simulations show that the new method can find coordinated chop-chop attacks.