Formal specification and analysis of security protocol is a research hotspot in network security at present. This paper models authentication service exchange of Public-Key Kerberos Protocol and an attack against this protocol with Petri nets. The Maria Tool automates analysis and verification of the model and finds that PKINIT -26 protocol has a security flaw. So we improve the model according to PKINIT -27 specification and verify authenticity of the improved model. It argues that Maria has the ability to analyze and verify sophisticated security protocols. Furthermore, it can be widely applied for automated analysis and verification of security protocol. © 2010 IEEE.