Abstract: Anonymous wireless body area networks communication technology is one of the most powerful means to protect the privacy of Internet users and servers,but formal authentication of anonymous wireless body area networks certificateless authentication protocol is still a difficult problem to be solved.The method of probabilistic model detection is used to set up a discrete time Markov chain model based on a cloud-aided lightweight certificateless authentication protocol with anonymity for wireless body area networks.The attack rate is added to the state migration of the protocol modeling,and in particular,the attack rate was analyzed quantitatively.The protocol attributes are described with the probability calculation tree logic,the PRISM namely a probabilistic model testing tool was used for quantitative analysis and verification of the protocol,and the performance of the protocol was compared with the SIP protocol.The result shows that the attack rate between the entities of the cloud-aided lightweight certificateless authentication protocol has different influence on non-repudiation,time delay and effectiveness of the protocol under anonymous WBANs communication environment.The control of the attack rate can improve the security of the protocol.It is of great significance to the quality of medical services,the improvement of real-time monitoring efficiency and the basic needs of telemedicine

Key words: Attack rate, Cloud-aided lightweight certificateless authentication protocol, PRISM, Probabilistic model checking, Wireless body area networks