TLA Based Kerberos Specification and Verification
Xing Li · Journal of Guizhou University · 2007
Leslie Lamport put forward a new logic: TLA.A program logic expresses both programs and properties with a single language.The AVISPA Tool provides a suite of applications for building and analyzing formal models of security protocols.Protocol models are written in the High Level Protocol Specification Language,or HLPSL.Then some roles are designed about Kerberos protocol,after that it is expressed by HLPSL and checked by AVISPA tool.The results indicate that the tool based on TLA is very effectual.