SG logic - A formal analysis technique for authentication protocols

Abstract

The security of electronic communication relies to a great extent on the security of authentication protocols used to distribute cryptographic keys. Hence formal techniques are needed which help to analyse the security of these protocols. In this paper we introduce a formal method which allows to detect the possibility of certain replay and interleaving attacks. By using our method we are able to show the weakness of the Neuman-Stubblebine protocol and to detect inaccuracies in some authentication protocols standardized in ISO. These inaccuracies may cause the protocol to allow interleaving attacks in certain environments, a fact which seems to be unrecognized so far.