Applying Strand Spaces to Certified Delivery Proofs
Resumo
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.Referências
Asokan, N. (1998). Fairness in Electronic Commerce. PhD thesis, University of Waterloo.
Boyd, C. and Kearney, P. (2000). Exploring fair exchange protocols using specification animation. In ISW ’00: Proceedings of the Third International Workshop on Information Security, pages 209–223, London, UK. Springer-Verlag.
Chadha, R., Kanovich, M. I., and Scedrov, A. (2001). Inductive methods and contractsigning protocols. In ACM Conference on Computer and Communications Security, pages 176–185.
Chadha, R., Kremer, S., and Scedrov, A. (2004). Formal analysis of multi-party contract signing.
Ferrer-Gomila, J. L., Payeras-Capellà, M., and Rotger, L. (2000). An efficient protocol for certified electronic mail. In Third International Workshop ISW 2000, volume 1975 of Lecture Notes in Computer Science, pages 237–248, Berlin. Springer-Verlag.
Garay, J. A., Jakobsson, M., and MacKenzie, P. (1999). Abuse-free optimistic contract signing. Lecture Notes in Computer Science, 1666:449–466.
Gürgens, S., Rudolph, C., and Vogt, H. (2005). On the security of fair non-repudiation protocols. Int. J. Inf. Secur., 4(4):253–262.
Guttman, J. D. and Thayer, F. J. (2002). Authentication tests and the structure of bundles. Theor. Comput. Sci., 283(2):333–380.
Monteiro, J. R. and Dahab, R. (2002). An attack on a protocol for certified delivery. Information Security 5th International Conference, ISC 2002, Proceedings, LNCS 2433.
Mukhamedov, A., Kremer, S., and Ritter, E. (2005). Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model. In Patrick, A. S. and Yung, M., editors, Revised Papers from the 9th International Conference on Financial Cryptography and Data Security (FC’05), volume 3570 of Lecture Notes in Computer Science, pages 255–269, Roseau, The Commonwealth Of Dominica. Springer.
Thayer, F. J., Herzog, J. C., and Guttman, J. D. (1999a). Mixed strand spaces. In CSFW ’99: Proceedings of the 1999 IEEE Computer Security Foundations Workshop, page 72, Washington, DC, USA. IEEE Computer Society.
Thayer, F. J., Herzog, J. C., and Guttman, J. D. (1999b). Strand spaces: Proving security protocols correct. Journal of Computer Security, 7(2–3):191–230.
Zhou, J., Deng, R. H., and Bao, F. (1999). Evolution of fair non-repudiation with ttp. In ACISP ’99: Proceedings of the 4th Australasian Conference on Information Security and Privacy, pages 258–269, London, UK. Springer-Verlag.
Zhou, J. and Gollmann, D. (1997). Evidence and non-repudiation. Journal of Network and Computer Applications, 20(3):267–281.
Boyd, C. and Kearney, P. (2000). Exploring fair exchange protocols using specification animation. In ISW ’00: Proceedings of the Third International Workshop on Information Security, pages 209–223, London, UK. Springer-Verlag.
Chadha, R., Kanovich, M. I., and Scedrov, A. (2001). Inductive methods and contractsigning protocols. In ACM Conference on Computer and Communications Security, pages 176–185.
Chadha, R., Kremer, S., and Scedrov, A. (2004). Formal analysis of multi-party contract signing.
Ferrer-Gomila, J. L., Payeras-Capellà, M., and Rotger, L. (2000). An efficient protocol for certified electronic mail. In Third International Workshop ISW 2000, volume 1975 of Lecture Notes in Computer Science, pages 237–248, Berlin. Springer-Verlag.
Garay, J. A., Jakobsson, M., and MacKenzie, P. (1999). Abuse-free optimistic contract signing. Lecture Notes in Computer Science, 1666:449–466.
Gürgens, S., Rudolph, C., and Vogt, H. (2005). On the security of fair non-repudiation protocols. Int. J. Inf. Secur., 4(4):253–262.
Guttman, J. D. and Thayer, F. J. (2002). Authentication tests and the structure of bundles. Theor. Comput. Sci., 283(2):333–380.
Monteiro, J. R. and Dahab, R. (2002). An attack on a protocol for certified delivery. Information Security 5th International Conference, ISC 2002, Proceedings, LNCS 2433.
Mukhamedov, A., Kremer, S., and Ritter, E. (2005). Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model. In Patrick, A. S. and Yung, M., editors, Revised Papers from the 9th International Conference on Financial Cryptography and Data Security (FC’05), volume 3570 of Lecture Notes in Computer Science, pages 255–269, Roseau, The Commonwealth Of Dominica. Springer.
Thayer, F. J., Herzog, J. C., and Guttman, J. D. (1999a). Mixed strand spaces. In CSFW ’99: Proceedings of the 1999 IEEE Computer Security Foundations Workshop, page 72, Washington, DC, USA. IEEE Computer Society.
Thayer, F. J., Herzog, J. C., and Guttman, J. D. (1999b). Strand spaces: Proving security protocols correct. Journal of Computer Security, 7(2–3):191–230.
Zhou, J., Deng, R. H., and Bao, F. (1999). Evolution of fair non-repudiation with ttp. In ACISP ’99: Proceedings of the 4th Australasian Conference on Information Security and Privacy, pages 258–269, London, UK. Springer-Verlag.
Zhou, J. and Gollmann, D. (1997). Evidence and non-repudiation. Journal of Network and Computer Applications, 20(3):267–281.
Publicado
28/08/2006
Como Citar
PIVA, Fabio R.; MONTEIRO, José R. M.; DEVEGILI, Augusto J.; DAHAB, Ricardo.
Applying Strand Spaces to Certified Delivery Proofs. In: SIMPÓSIO BRASILEIRO DE SEGURANÇA DA INFORMAÇÃO E DE SISTEMAS COMPUTACIONAIS (SBSEG), 6. , 2006, Santos.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2006
.
p. 72-85.
DOI: https://doi.org/10.5753/sbseg.2006.20940.
