Applying Strand Spaces to Certified Delivery Proofs - Piva, Fabio R.; Monteiro, José R. M.; Devegili, Augusto J.; Dahab, Ricardo (Anais do Simpósio Brasileiro de Cibersegurança (SBSeg); 2006: Anais do VI Simpósio Brasileiro de Segurança da Informação e de Sistemas Computacionais, 2006)
Although fair exchange protocols are being widely implemented, there are few formal methods able to verify them. This work introduces the strand spaces method for verifying certified mail delivery protocols, a subclass of fair exchange protocols. Three fair exchange properties are verified: effectiveness, verifiability of TTP and timeliness. For effectiveness and verifiability we used the FPH protocol [Ferrer-Gomila et al. 2000]; for timeliness we use the ZDB protocol [Zhou et al. 1999]. We show that strand spaces can be applied to fair exchange protocols, and present an additional attack to the FPH protocol which was not previously reported.