Specifying Security Protocols with ASM
Xue Rui · 2002
The primary elements of Gurevich's Abstract State Machines(ASM)are introduced. A verification enviroment is proposed for analying of security protocols in ASM,and a general penetrator model is presented so that much of security properties could be dealed with. As a case, Helsinki protocol are specified in the model,a direct mathematical proof of its weakness is given.