Abstract
We formally specify a payment protocol described in [Vogt et al., 2001]. This protocol is intended for fair exchange of time-sensitive data. Here the μCRL language is used to formalize the protocol. Fair exchange properties are expressed in the regular alternation-free μ-calculus. These properties are then verified using the finite state model checker from the CADP toolset. Proving fairness without resilient communication channels is impossible. We use the Dolev-Yao intruder, but since the conventional Dolev-Yao intruder violates this assumption, it is forced to comply to the resilient communication channel assumption.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Asokan, N. (1998). Fairness in electronic commerce. PhD thesis, University of Waterloo.
Bella, G. and Paulson, L. C. (2001). Mechanical proofs about a non-repudiation protocol. In Boulton, R. J. and Jackson, P. B., editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, volume 2152 of LNCS, pages 91–104. Springer-Verlag.
Blom, S., Fokkink, W., Groote, J. F., van Langevelde, I., Lisser, B., and van de Pol, J. (2001). μCRL: A toolset for analysing algebraic specifications. In Proceedings of the 13th International Conference on Computer Aided Verification, volume 2102 of LNCS, pages 250–254. Springer-Verlag.
Cederquist, J. and Dashti, M. (2004). Formal analysis of a fair payment protocol. Technical Report SEN-R0410, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.
Cervesato, I. (2001). The Dolev-Yao Intruder is the Most Powerful Attacker. In Halpern, J., editor, 16th Annual Symposium on Logic in Computer Science-LICS'01, Boston, MA. IEEE Computer Society Press.
Dolev, D. and Yao, A. C. (1983). On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(2): 198–208.
Fernandez, J.-C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., and Sighireanu, M. (1996). CADP: A protocol validation and verification toolbox. In Alur, R. and Henzinger, T. A., editors, Proceedings of the 8th Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 437–440. Springer-Verlag.
Groote, J. and Ponse, A. (1995). The syntax and semantics of μCRL. In Ponse, A., Verhoef, C., and van Vlijmen, S. F. M., editors, Algebra of Communicating Processes '94, Workshops in Computing Series, pages 26–62. Springer-Verlag.
Kremer, S. and Raskin, J. (2001). A game-based verification of non-repudiation and fair exchange protocols. In Larsen, K. and Nielsen, M., editors, Proceedings of the 12th International Conference on Concurrency Theory, volume 2154 of LNCS, pages 551–565. Springer-Verlag.
Mateescu, R. (2000). Efficient diagnostic generation for boolean equation systems. In Proceedings of 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2000, volume 1785 of LNCS, pages 251–265. Springer-Verlag.
Pagnia, H. and Gärtner, F. C. (1999). On the impossibility of fair exchange without a trused third party. Technical Report TUD-BS-1999-02, Department of Computer Science, Darmstadt University of Technology.
Pagnia, H., Vogt, H., and Gärtner, F. C. (2003). Fair exchange. The Computer Journal, 46(1):55–7.
Schneider, S. (1998). Formal analysis of a non-repudiation protocol. In Proceedings of The 11th Computer Security Foundations Workshop, pages 54–65. IEEE Computer Society Press.
Shmatikov, V. and Mitchell, J. C. (2002). Finitestate analysis of two contract signing protocols. Theoretical Computer Sciene, 283(2):419–450.
Vogt, H., Pagnia, H., and Gärtner, F. C. (2001). Using smart cards for fair exchange. In Electronic Commerce — WELCOM 2001, volume 2232 of LNCS, pages 101–113. Springer-Verlag.
Zhou, J. and Gollmann, D. (1998). Towards verification of non-repudiation protocols. In International Refinement Workshop and Formal Methods Pacific '98: Proceedings of IRW/FMP '98, Discrete Mathematics and Theoretical Computer Science Series, pages 370–380. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 International Federation for Information Processing
About this paper
Cite this paper
Cederquist, J., Dashti, M.T. (2005). Formal Analysis of a Fair Payment Protocol. In: Dimitrakos, T., Martinelli, F. (eds) Formal Aspects in Security and Trust. IFIP WCC TC1 2004. IFIP International Federation for Information Processing, vol 173. Springer, Boston, MA. https://doi.org/10.1007/0-387-24098-5_4
Download citation
DOI: https://doi.org/10.1007/0-387-24098-5_4
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-24050-3
Online ISBN: 978-0-387-24098-5
eBook Packages: Computer ScienceComputer Science (R0)