Establishing and fixing a freshness flaw in a key-distribution and authentication protocol

The security of electronic networks and information systems is nowadays seen as a critical issue for the growth of Information and Communication Technologies. Cryptographic protocols are used to provide security services such as confidentiality, message integrity, authentication, certified E-mail and non-repudiation. Traditionally, security protocols have been designed and verified using informal techniques. However, the absence of formal verification can lead to security errors remaining undetected. Formal verification techniques provide a systematic way of discovering protocol flaws. This paper establishes a freshness flaw in a keydistribution and Authentication Protocol using an automated logic-based verification engine. The performed verification reveals a freshness flaw in the protocol that allows an intruder to impersonate legitimate principals. The cause of the freshness flaw is discussed and an amended protocol is proposed. Formal verification of the amended protocol provides confidence in the correctness and effectiveness of the proposed modifications.