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 ComputacionaisDO - 10.5753/sbseg.2006.20940, 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.