Bursuc, Sergiu ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Kremer, Steve; INRIA France
External co-authors :
no
Language :
English
Title :
Contingent Payments on a Public Ledger: Models and Reductions for Automated Verification.
Publication date :
September 2019
Event name :
ESORICS 2019 - 24th European Symposium on Research in Computer Security
Event place :
Luxembourg, Luxembourg
Event date :
23-27 September 2019
Main work title :
Contingent Payments on a Public Ledger: Models and Reductions for Automated Verification.
Garay, J., Kiayias, A., Leonardos, N.: The bitcoin backbone protocol: analysis and applications. In: Oswald, E., Fischlin, M. (eds.) EUROCRYPT 2015. LNCS, vol. 9057, pp. 281–310. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46803-6 10
Pass, R., Seeman, L., Shelat, A.: Analysis of the blockchain protocol in asynchronous networks. In: Coron, J.-S., Nielsen, J.B. (eds.) EUROCRYPT 2017. LNCS, vol. 10211, pp. 643–673. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-56614-6 22
Dashti, M.T., Mauw, S.: Fair exchange. In: Rosenberg, B. (ed.) Handbook of Financial Cryptography and Security, pp. 109–132. Chapman and Hall/CRC, Boca Raton (2010)
Asokan, N., Shoup, V., Waidner, M.: Optimistic fair exchange of digital signatures. In: Nyberg, K. (ed.) EUROCRYPT 1998. LNCS, vol. 1403, pp. 591–606. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054156
Micali, S.: Simple and fast optimistic protocols for fair electronic exchange. In: 22nd ACM Symposium on Principles of Distributed Computing (PODC 2003), pp. 12–19. ACM (2003)
Lindell, A.Y.: Legally-enforceable fairness in secure two-party computation. In: Malkin, T. (ed.) CT-RSA 2008. LNCS, vol. 4964, pp. 121–137. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79263-5 8
Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Fair two-party computations via bitcoin deposits. In: Böhme, R., Brenner, M., Moore, T., Smith, M. (eds.) FC 2014. LNCS, vol. 8438, pp. 105–121. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44774-1 8
Bentov, I., Kumaresan, R.: How to use bitcoin to design fair protocols. In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014. LNCS, vol. 8617, pp. 421–439. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44381-1 24
Bitcoin Wiki: Zero Knowledge Contingent Payment. https://en.bitcoin.it/wiki/Zero Knowledge Contingent Payment
Banasik, W., Dziembowski, S., Malinowski, D.: Efficient zero-knowledge contingent payments in cryptocurrencies without scripts. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 261–280. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45741-3 14
Campanelli, M., Gennaro, R., Goldfeder, S., Nizzardo, L.: Zero-knowledge contingent payments revisited: attacks and payments for services. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2017), pp. 229–243. ACM (2017)
Goldfeder, S., Bonneau, J., Gennaro, R., Narayanan, A.: Escrow protocols for cryptocurrencies: how to buy physical goods using bitcoin. In: Kiayias, A. (ed.) FC 2017. LNCS, vol. 10322, pp. 321–339. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70972-7 18
Dziembowski, S., Eckey, L., Faust, S.: FairSwap: how to fairly exchange digital goods. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 967–984. ACM (2018)
Cohn-Gordon, K., Cremers, C.J.F., Garratt, L.: On post-compromise security. In: IEEE 29th Computer Security Foundations Symposium (CSF 2016), pp. 164–178. IEEE Computer Society (2016)
Cohn-Gordon, K., Cremers, C.J.F., Dowling, B., Garratt, L., Stebila, D.: A formal security analysis of the signal messaging protocol. In: IEEE European Symposium on Security and Privacy (EuroS&P 2017), pp. 451–466. IEEE Computer Society (2017)
Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: IEEE Symposium on Security and Privacy (SP 2017), pp. 483–502. IEEE Computer Society (2017)
Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2017), pp. 1773–1788. ACM (2017)
Jacomme, C., Kremer, S.: An extensive formal analysis of multi-factor authentication protocols. In: 31st IEEE Computer Security Foundations Symposium (CSF 2018), pp. 1–15. IEEE Computer Society (2018)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8 48
Cervesato, I., Durgin, N.A., Mitchell, J.C., Lincoln, P., Scedrov, A.: Relating strands and multiset rewriting for security protocol analysis. In: 13th IEEE Computer Security Foundations Workshop, CSFW 2000, Cambridge, England, UK, 3–5 July 2000, pp. 35–51. IEEE Computer Society (2000)
Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 25th IEEE Computer Security Foundations Symposium (CSF 2012), pp. 78–94. IEEE Computer Society (2012)
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 243–320. MIT Press, Cambridge (1990)
Vaudenay, S.: The security of DSA and ECDSA. In: Desmedt, Y.G. (ed.) PKC 2003. LNCS, vol. 2567, pp. 309–323. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36288-6 23
Rivest, R.L., Shamir, A., Wagner, D.A.: Time-lock puzzles and timed-release crypto. Technical report, MIT, Cambridge, MA, USA (1996)
Boneh, D., Naor, M.: Timed commitments. In: Bellare, M. (ed.) CRYPTO 2000. LNCS, vol. 1880, pp. 236–254. Springer, Heidelberg (2000). https://doi.org/10. 1007/3-540-44598-615
Tamarin code for ZKCP protocol verification. https://www.dropbox.com/sh/ahzbbojm5z0e6a9/AAB6-Pz-RK3xwVznlaqaitfca?dl=0
Paillier, P.: Public-key cryptosystems based on composite degree residuosity classes. In: Stern, J. (ed.) EUROCRYPT 1999. LNCS, vol. 1592, pp. 223–238. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48910-X 16
Lindell, Y.: Fast secure two-party ECDSA signing. In: Katz, J., Shacham, H. (eds.) CRYPTO 2017. LNCS, vol. 10402, pp. 613–644. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63715-0 21
Lindell, Y., Nof, A.: Fast secure multiparty ECDSA with practical distributed key generation and applications to cryptocurrency custody. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 1837–1854. ACM (2018)
Gennaro, R., Goldfeder, S.: Fast multiparty threshold ECDSA with fast trustless setup. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 1179–1194. ACM (2018)
Additional material: Tamarin code and long paper version. https://www.dropbox. com/sh/t74k3q4gxrmo0pw/AADvx0e8WDaZgyf0OQFlElICa?dl=0
Schmidt, B., Sasse, R., Cremers, C., Basin, D.A.: Automated verification of group key agreement protocols. In: IEEE Symposium on Security and Privacy (SP 2014), pp. 179–194 (2014)
Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, pp. 359–373. IEEE Computer Society (2018)
Dreier, J., Duménil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equa-tional theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117–140. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-66
Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. J. Comput. Secur. 24(5), 583–616 (2016)
Backes, M., Dreier, J., Kremer, S., Künnemann, R.: A novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange. In: IEEE European Symposium on Security and Privacy (EuroS&P 2017), pp. 76–91. IEEE Computer Society (2017)
Baudron, O., Fouque, P.-A., Pointcheval, D., Stern, J., Poupard, G.: Practical multi-candidate election system. In: 20th Annual (ACM) Symposium on Principles of Distributed Computing (PODC 2001), pp. 274–283. ACM (2001)
Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Narendran, P.: Theories of homomorphic encryption, unification, and the finite variant property. In: Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, 8–10 September 2014, pp. 123– 133 (2014)
Bartoletti, M., Zunino, R.: BitML: a calculus for bitcoin smart contracts. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 83–100 (2018)
Bhargavan, K., et al.: Formal verification of smart contracts. In: ACM Workshop on Programming Languages and Analysis for Security (PLAS@CCS 2016), pp. 91–96. ACM (2016)
Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the ethereum virtual machine. In: 31st IEEE Computer Security Foundations Symposium (CSF 2018), pp. 204–217. IEEE Computer Society (2018)
Dziembowski, S., Faust, S., Hostáková, K.: General state channel networks. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2018), pp. 949–966. ACM (2018)
Ben-Sasson, E., et al.: Zerocash: decentralized anonymous payments from bitcoin. In: IEEE Symposium on Security and Privacy, SP 2014, pp. 459–474. IEEE Computer Society (2014)
Malavolta, G., Moreno-Sanchez, P., Kate, A., Maffei, M., Ravi, S.: Concurrency and privacy with payment-channel networks. In: ACM SIGSAC Conference on Computer and Communications Security (CCS 2017), pp. 455–471. ACM (2017)
