| The new challenges of the road transportation’s security has been brought with the traffic demand increasing, and the existing traditional technologies of vehicle diagnosis, with the purpose of guaranteed road traffic security, are not able to meet the requirement of real-time traffic security. Remote vehicle diagnosis technologies will be the future trend in vehicle diagnosis area.Most of researches on remote vehicle diagnosis are focused on diagnosis system design and diagnosis communication process, instead of identity authentication and authorization process. Therefore, the process of the identity authentication and authorization is chosed as the research object. Then, presenting the remote authorization protocol for vehicle diagnosis by introducing ticket service authority is proposed in this paper. Moreover, the description of the protocol and the verification of its security by using a formal method are also proposed.In the process of protocol design, security performance is improved by utilizing the trusted platform models and mechanism of client-puzzle based on the mixed strategy Nash equilibrium. In the security analysis phase, according to the security requirements, the security objectives are listed. Then, the security objectives are descripted by using a formal method and the descripted security objectives are automatically verified through the Pro Verif. An analysis which is conducted to show the performance of the client-puzzle mechanism is provided. At last, the method of calculating the client-puzzle policy and some instances are also provided. |