Welcome to Journal of University of Chinese Academy of Sciences,Today is

›› 2002, Vol. 19 ›› Issue (3): 263-270.DOI: 10.7523/j.issn.2095-6134.2002.3.007

Previous Articles     Next Articles

Specifying Security Protocols with ASM

XUE Rui1,2, FENG Deng-Guo1   

  1. 1. State Key Laboratory of Information Security, IOS, CAS, Beijing 100039;
    2. College of Mathematics and Computer Sciences, Shanxi Teacher’s University, Lin fen 041004
  • Received:2002-06-06 Online:2002-05-18

Abstract:

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.

Key words: abstract state machine, cryptographic protocol, formal method, formal specification

CLC Number: