Research Project: Lex Leibniz

Smart contracts on cryptocurrency platforms carry large amounts of monetary value, but have been prone to flaws and security vulnerabilities that have resulted in large financial losses.

This project is investigating the development of a high level smart contract language, suitable for the representation of financial contracts, that better supports the development of correct and secure smart contracts.

We are investigating the fundamental principles of smart contract verification, and developing ways of expressing financial contracts as smart contracts in ways that are more easily comprehensible to their users, and supports verification of both correctness and security.

The core methodological principle underlying the work is the use of declarative representations of smart contracts and their specifications. We will draw on earlier contributions to logic programming, deontic logic (the logic of permission, obligation and prohibition), work on logics for authentication and authorization in cryptographic settings and linear logic (as a representation of resource production, preservation and consumption).

Staff:

Prof. Ron van der Meyden (CSE), Prof. Michael Maher (ADFA and Reasoning Research Institute),

Outcomes:

• On the specification and verification of atomic swap smart contracts (extended abstract), Proc. IEEE International Conference on Blockchain and Cryptocurrency 2019, R. van der Meyden. (Full version: arXiv:1811.06099, Nov 2018)
  
  
• A Formal Treatment of Contract Signature, Ron van der Meyden, to appear, IEEE Transactions on Services Computing. DOI:10.1109/TSC.2021.3101833 (Accepted version on Arxiv: arXiv:2002.09827).
  
  

Related earlier work:

• [J11] A logical reconstruction of SPKI, J.Y. Halpern and R. van der Meyden, Journal of Computer Security, Volume 11, Issue 4, 2003,. pp 581-614. (a special issue of Journal of Computer Security containing selected papers from CSFW'01.)
  
  
• [J7] A logic for SDSI's Linked Local Name Spaces , J. Y. Halpern and R. van der Meyden, Journal of Computer Security, vol. 9, number 1,2, pp. 75 - 104, 2001. (a special issue of the Journal of Computer Security containing selected papers from CSFW 99.)
  
  
• [J3] The Dynamic Logic of Permission, R. van der Meyden, Journal of Logic and Computation, Vol 6, No. 3 pp. 465-479, 1996. A version of this paper appeared at the IEEE Symposium on Logic in Computer Science, Philadelphia, 1990.
  
  
• [C4] A Clausal Logic for Deontic Action Specification, R. van der Meyden, Proceedings of the International Logic Programming Symposium, San Diego, October 1991, pp. 221-238. MIT Press.