Formally analysing a security protocol for replay attacks

The Kerberos-One-Time protocol is a key distribution protocol promoted for use with Javacards to provide secure communication over the GSM mobile phone network. From inspection we suspected a replay attack was possible on the protocol. To check this, we formally specified the protocol using Object-Z and then analysed its behaviour in the presence of an attacker using the symbolic analysis laboratory´s model checker. To produce accurate results efficiently, our formalism included an abstraction of the protocol´s data structures that captured just those characteristics that we believed made the protocol vulnerable. Ultimately, the model checker´s analysis confirmed our suspicions about the protocol´s weakness