research-article

A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation

Authors:

Karim Eldefrawy,

Vitor PereiraAuthors Info & Claims

CCS '19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security

Pages 851 - 868

https://doi.org/10.1145/3319535.3354205

Published: 06 November 2019 Publication History

Abstract

Secure Multiparty Computation (MPC) enables a group of n</> distrusting parties to jointly compute a function using private inputs. MPC guarantees correctness of computation and confidentiality of inputs if no more than a threshold t</> of the parties are corrupted. Proactive MPC (PMPC) addresses the stronger threat model of a \emphmobile adversary that controls a changing set of parties (but only up to t</> at any instant), and may eventually corrupt all n</> parties over a long time. This paper takes a first stab at developing high-assurance implementations of (P)MPC. We formalize in \EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, several abstract and reusable variations of secret sharing and of (P)MPC protocols building on them. Using those, we prove a series of abstract theorems for the proactive setting. We implement and perform computer-checked security proofs of concrete instantiations of the required (abstract) protocols in \EasyCrypt. We also develop a new tool-chain to extract high-assurance executable implementations of protocols formalized and verified in \EasyCrypt. Our tool-chain uses \Why as an intermediate tool, and enables us to extract executable code from our (P)MPC formalizations. We conduct an evaluation of the extracted executables by comparing their performance to performance of manually implemented versions using \textsfPython -based \textsfCharm framework for prototyping cryptographic schemes. We argue that the small overhead of our high-assurance executables is a reasonable price to pay for the increased confidence about their correctness and security.

Supplementary Material

WEBM File (p851-pereira.webm)

Download
112.24 MB

References

[1]

Masayuki Abe and Serge Fehr. 2004. Adaptively Secure Feldman VSS and Applications to Universally-Composable Threshold Cryptography. In Advances in Cryptology -- CRYPTO 2004, Matt Franklin (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 317--334.

[2]

Joseph A. Akinyele, Christina Garman, Ian Miers, Matthew W. Pagano, Michael Rushanan, Matthew Green, and Aviel D. Rubin. 2013. Charm: a framework for rapidly prototyping cryptosystems. Journal of Cryptographic Engineering, Vol. 3, 2 (01 Jun 2013), 111--128. https://doi.org/10.1007/s13389-013-0057--3

[3]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and Francc ois Dupressoir. 2016. Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. In 23rd International Conference on Fast Software Encryption (FSE) . 163--184.

Digital Library

[4]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francc ois Dupressoir, Benjamin Grégoire, Vincent Laporte, and Vitor Pereira. 2017. A fast and verified software stack for secure function evaluation. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. ACM, 1989--2006.

Digital Library

[5]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, and Bernardo Portela. 2018. Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 132--146.

[6]

Gilad Asharov and Yehuda Lindell. 2011. A Full Proof of the BGW Protocol for Perfectly-Secure Multiparty Computation. Cryptology ePrint Archive, Report 2011/136. https://eprint.iacr.org/2011/136.

[7]

Michael Backes, Aniket Kate, and Arpita Patra. 2011. Computational Verifiable Secret Sharing Revisited. In Advances in Cryptology -- ASIACRYPT 2011, Dong Hoon Lee and Xiaoyun Wang (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 590--609.

[8]

Michael Backes, Matteo Maffei, and Esfandiar Mohammadi. 2010. Computationally Sound Abstraction and Verification of Secure Multi-Party Computations. In FSTTCS .

[9]

Cécile Baritel-Ruet, Francc ois Dupressoir, Pierre-Alain Fouque, and Benjamin Grégoire. 2018. Formal Security Proof of CMAC and its Variants. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 91--104.

[10]

Joshua Baron, Karim Eldefrawy, Joshua Lampkins, and Rafail Ostrovsky. 2014. How to withstand mobile virus attacks, revisited. In PODC. ACM, 293--302.

[11]

Joshua Baron, Karim Eldefrawy, Joshua Lampkins, and Rafail Ostrovsky. 2015a. Communication-Optimal Proactive Secret Sharing for Dynamic Groups. In Applied Cryptography and Network Security, Tal Malkin, Vladimir Kolesnikov, Allison Bishop Lewko, and Michalis Polychronakis (Eds.). Springer International Publishing, Cham, 23--41.

[12]

Joshua Baron, Karim Eldefrawy, Joshua Lampkins, and Rafail Ostrovsky. 2015b. Communication-Optimal Proactive Secret Sharing for Dynamic Groups. In ACNS (LNCS), Vol. 9092. Springer, 23--41.

[13]

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. 2014. Probabilistic Relational Verification for Cryptographic Implementations. In POPL . To appear.

[14]

Assaf Ben-David, Noam Nisan, and Benny Pinkas. 2008. FairplayMP: a system for secure multi-party computation. In Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, Alexandria, Virginia, USA, October 27--31, 2008, Peng Ning, Paul F. Syverson, and Somesh Jha (Eds.). ACM, 257--266. https://doi.org/10.1145/1455770.1455804

Digital Library

[15]

Michael Ben-Or, Shafi Goldwasser, and Avi Wigderson. 1988. Completeness theorems for non-cryptographic fault-tolerant distributed computation. In Proceedings of the 20th Annual Symposium on Theory of Computing. ACM, 1--10.

Digital Library

[16]

Michael Ben-Or, Shafi Goldwasser, and Avi Wigderson. 1988. Completeness Theorems for Non-Cryptographic Fault-Tolerant Distributed Computation (Extended Abstract). In STOC. ACM, 1--10.

[17]

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, and Jean Karim Zinzindohoué. 2016. Implementing and Proving the TLS 1.3 Record Layer. Cryptology ePrint Archive, Report 2016/1178. http://eprint.iacr.org/2016/1178.

[18]

Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. 2013. Implementing TLS with Verified Cryptographic Security. In IEEE S&P .

[19]

G. R. Blakley. 1979. Safeguarding cryptographic keys. Proc. of AFIPS National Computer Conference, Vol. 48 (1979), 313--317.

[20]

Dan Bogdanov, Peeter Laud, Sven Laur, and Pille Pullonen. 2014. From input private to universally composable secure multi-party computation primitives. In Proceedings of the 27th Computer Security Foundations Symposium. IEEE, 184--198.

Digital Library

[21]

Dan Bogdanov, Sven Laur, and Jan Willemson. 2008. Sharemind: A Framework for Fast Privacy-Preserving Computations. In ESORICS (Lecture Notes in Computer Science), Vol. 5283. Springer, 192--206.

[22]

Sally Browning and Philip Weaver. 2010. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol . 89--143. https://doi.org/10.1007/978--1--4419--1539--9_4

[23]

Christian Cachin, Klaus Kursawe, Anna Lysyanskaya, and Reto Strobl. 2002 a. Asynchronous verifiable secret sharing and proactive cryptosystems. In ACM Conference on Computer and Communications Security. 88--97.

Digital Library

[24]

Christian Cachin, Klaus Kursawe, Anna Lysyanskaya, and Reto Strobl. 2002 b. Asynchronous Verifiable Secret Sharing and Proactive Cryptosystems. In Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS '02). ACM, New York, NY, USA, 88--97. https://doi.org/10.1145/586110.586124

Digital Library

[25]

B. Chor, S. Goldwasser, S. Micali, and B. Awerbuch. 1985. Verifiable secret sharing and achieving simultaneity in the presence of faults. In 26th Annual Symposium on Foundations of Computer Science (sfcs 1985) . 383--395. https://doi.org/10.1109/SFCS.1985.64

Digital Library

[26]

Véronique Cortier, Constantin Catalin Dragan, Francc ois Dupressoir, and Bogdan Warinschi. 2018. Machine-checked proofs for electronic voting: privacy and verifiability for Belenios. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). IEEE, 298--312.

[27]

Morten Dahl and Ivan Damgård. 2014. Universally Composable Symbolic Analysis for Two-Party Protocols Based on Homomorphic Encryption. In EUROCRYPT .

[28]

Ivan Damgård, Kasper Damgård, Kurt Nielsen, Peter Sebastian Nordholt, and Tomas Toft. 2016. Confidential Benchmarking based on Multiparty Computation. In Proceedings of the 20th International Conference on Financial Cryptography and Data Security . Springer, 169--187.

[29]

Daniel Demmler, Thomas Schneider, and Michael Zohner. 2015. ABY - A Framework for Efficient Mixed-Protocol Secure Two-Party Computation. In 22nd Annual Network and Distributed System Security Symposium, NDSS 2015, San Diego, California, USA, February 8--11, 2015 . https://www.ndss-symposium.org/ndss2015/aby--framework-efficient-mixed-protocol-secure-two-party-computation

[30]

Shlomi Dolev, Karim Eldefrawy, Joshua Lampkins, Rafail Ostrovsky, and Moti Yung. 2016a. Proactive Secret Sharing with a Dishonest Majority. In Security and Cryptography for Networks, Vassilis Zikas and Roberto De Prisco (Eds.). Springer International Publishing, Cham, 529--548.

[31]

Shlomi Dolev, Karim Eldefrawy, Joshua Lampkins, Rafail Ostrovsky, and Moti Yung. 2016b. Proactive Secret Sharing with a Dishonest Majority. In SCN (LNCS), Vol. 9841. Springer, 529--548.

[32]

Yael Ejgenberg, Moriya Farbstein, Meital Levy, and Yehuda Lindell. 2012. SCAPI: The Secure Computation Application Programming Interface. Cryptology ePrint Archive, Report 2012/629. https://eprint.iacr.org/2012/629.

[33]

Karim Eldefrawy, Rafail Ostrovsky, Sunoo Park, and Moti Yung. 2018. Proactive Secure Multiparty Computation with a Dishonest Majority. In Proceedings of the Eleventh Conference on Security and Cryptography for Networks . 200--215. https://doi.org/10.1007/978--3--319--98113-0_11

Digital Library

[34]

Karim Eldefrawy and Vitor Pereira. 2019. A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation. Cryptology ePrint Archive, Report 2019/922. https://eprint.iacr.org/2019/922.

[35]

P. Feldman. 1987. A practical scheme for non-interactive verifiable secret sharing. In 28th Annual Symposium on Foundations of Computer Science (sfcs 1987). 427--438. https://doi.org/10.1109/SFCS.1987.4

Digital Library

[36]

Jean-Christophe Filliâtre. 2013. One Logic To Use Them All. In 24th International Conference on Automated Deduction (CADE-24) (Lecture Notes in Artificial Intelligence), Vol. 7898. Springer, Lake Placid, USA, 1--20.

[37]

Jean-Christophe Filliâtre and Andrei Paskevich. 2013. Why3 -- Where Programs Meet Provers. In Proceedings of the 22nd European Symposium on Programming (Lecture Notes in Computer Science), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 125--128.

Digital Library

[38]

Matthias Fitzi, Juan Garay, Shyamnath Gollakota, C. Pandu Rangan, and Kannan Srinathan. 2006. Round-Optimal and Efficient Verifiable Secret Sharing. In Theory of Cryptography, Shai Halevi and Tal Rabin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 329--342.

[39]

Cédric Fournet, Markulf Kohlweiss, and Pierre-Yves Strub. 2011. Modular code-based cryptographic verification. In ACM CCS .

[40]

Matthew Franklin and Moti Yung. 1992. Communication Complexity of Secure Computation (Extended Abstract). In Proceedings of the Twenty-fourth Annual ACM Symposium on Theory of Computing (STOC '92). ACM, New York, NY, USA, 699--710. https://doi.org/10.1145/129712.129780

Digital Library

[41]

Rosario Gennaro, Yuval Ishai, Eyal Kushilevitz, and Tal Rabin. 2001. The Round Complexity of Verifiable Secret Sharing and Secure Multicast. In Proceedings of the Thirty-third Annual ACM Symposium on Theory of Computing (STOC '01). ACM, New York, NY, USA, 580--589. https://doi.org/10.1145/380752.380853

Digital Library

[42]

Rosario Gennaro, Michael O. Rabin, and Tal Rabin. 1998. Simplified VSS and Fast-track Multiparty Computations with Applications to Threshold Cryptography. In Proceedings of the Seventeenth Annual ACM Symposium on Principles of Distributed Computing (PODC '98). ACM, New York, NY, USA, 101--111. https://doi.org/10.1145/277697.277716

Digital Library

[43]

Oded Goldreich, Silvio Micali, and Avi Wigderson. 1987. How to Play any Mental Game or A Completeness Theorem for Protocols with Honest Majority. In STOC. 218--229.

[44]

Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, and Pierre-Yves Strub. 2018a. Computer-Aided Proofs for Multiparty Computation with Active Security. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9--12, 2018. IEEE Computer Society, 119--131. https://doi.org/10.1109/CSF.2018.00016

[45]

Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, and Pierre-Yves Strub. 2018b. Computer-Aided Proofs for Multiparty Computation with Active Security. 119--131. https://doi.org/10.1109/CSF.2018.00016

[46]

Wilko Henecka, Stefan K ögl, Ahmad-Reza Sadeghi, Thomas Schneider, and Immo Wehrenberg. 2010a. TASTY: Tool for Automating Secure Two-party Computations. In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS '10). ACM, New York, NY, USA, 451--462. https://doi.org/10.1145/1866307.1866358

Digital Library

[47]

Wilko Henecka, Stefan Kögl, Ahmad-Reza Sadeghi, Thomas Schneider, and Immo Wehrenberg. 2010b. TASTY: Tool for Automating Secure Two-partY computations. IACR Cryptology ePrint Archive, Vol. 2010, 451--462. https://doi.org/10.1145/1866307.1866358

[48]

Amir Herzberg, Stanislaw Jarecki, Hugo Krawczyk, and Moti Yung. 1995 a. Proactive Secret Sharing Or: How to Cope With Perpetual Leakage. In CRYPTO . 339--352.

[49]

Amir Herzberg, Stanisław Jarecki, Hugo Krawczyk, and Moti Yung. 1995 b. Proactive Secret Sharing Or: How to Cope With Perpetual Leakage. In Advances in Cryptology -- CRYPT0' 95, Don Coppersmith (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 339--352.

[50]

Martin Hirt, Christoph Lucas, and Ueli Maurer. 2013. A Dynamic Tradeoff between Active and Passive Corruptions in Secure Multi-Party Computation. In CRYPTO (2) (LNCS), Vol. 8043. Springer, 203--219.

[51]

Jonathan Katz, Chiu-Yuen Koo, and Ranjit Kumaresan. 2008. Improving the Round Complexity of VSS in Point-to-Point Networks. In Automata, Languages and Programming, Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 499--510.

[52]

Hugo Krawczyk. 2001. The Order of Encryption and Authentication for Protecting Communications (or: How Secure Is SSL?). In Advances in Cryptology -- CRYPTO 2001, Joe Kilian (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 310--331.

[53]

Ranjit Kumaresan, Arpita Patra, and C. Pandu Rangan. 2010. The Round Complexity of Verifiable Secret Sharing: The Statistical Case. In Advances in Cryptology - ASIACRYPT 2010, Masayuki Abe (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 431--447.

[54]

Baiyu Li and Daniele Micciancio. 2018. Symbolic Security of Garbled Circuits. 147--161. https://doi.org/10.1109/CSF.2018.00018

[55]

Dahlia Malkhi, Noam Nisan, Benny Pinkas, and Yaron Sella. 2004. Fairplay - Secure Two-Party Computation System. In Proceedings of the 13th USENIX Security Symposium, August 9--13, 2004, San Diego, CA, USA, Matt Blaze (Ed.). USENIX, 287--302. http://www.usenix.org/publications/library/proceedings/sec04/tech/malkhi.html

Digital Library

[56]

Ueli M. Maurer. 2006. Secure multi-party computation made simple. Discrete Applied Mathematics, Vol. 154, 2 (2006), 370--381. https://doi.org/10.1016/j.dam.2005.03.020

[57]

Rafail Ostrovsky and Moti Yung. 1991. How to Withstand Mobile Virus Attacks (Extended Abstract). In PODC. ACM, 51--59.

[58]

Mário José Parreira Pereira. 2018. Tools and Techniques for the Verification of Modular Stateful Code . Ph.D. Dissertation. Paris Saclay.

[59]

Arpita Patra, Ashish Choudhary, Tal Rabin, and C. Pandu Rangan. 2009. The Round Complexity of Verifiable Secret Sharing Revisited. In Advances in Cryptology - CRYPTO 2009, Shai Halevi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 487--504.

Digital Library

[60]

Torben Pryds Pedersen. 1991. A Threshold Cryptosystem Without a Trusted Party. In Proceedings of the 10th Annual International Conference on Theory and Application of Cryptographic Techniques (EUROCRYPT'91). Springer-Verlag, Berlin, Heidelberg, 522--526. http://dl.acm.org/citation.cfm?id=1754868.1754929

Digital Library

[61]

Torben Pryds Pedersen. 1992. Non-Interactive and Information-Theoretic Secure Verifiable Secret Sharing. In Advances in Cryptology -- CRYPTO '91, Joan Feigenbaum (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 129--140.

[62]

Aseem Rastogi, Nikhil Swamy, and Michael Hicks. 2017. WYS*: A Verified Language Extension for Secure Multi-party Computations. CoRR, Vol. abs/1711.06467 (2017). arxiv: 1711.06467 http://arxiv.org/abs/1711.06467

[63]

David Schultz. 2007. Mobile Proactive Secret Sharing . Ph.D. Dissertation. Massachusetts Institute of Technology.

[64]

Adi Shamir. 1979 a. How to Share a Secret. Commun. ACM, Vol. 22, 11 (1979), 612--613.

Digital Library

[65]

Adi Shamir. 1979 b. How to Share a Secret. Commun. ACM, Vol. 22, 11 (Nov. 1979), 612--613. https://doi.org/10.1145/359168.359176

Digital Library

[66]

Alley Stoughton and Mayank Varia. 2017. Mechanizing the Proof of Adaptive, Information-Theoretic Security of Cryptographic Protocols in the Random Oracle Model. In 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21--25, 2017. IEEE Computer Society, 83--99. https://doi.org/10.1109/CSF.2017.36

[67]

Xiao Wang, Alex J. Malozemoff, and Jonathan Katz. 2017a. Faster Secure Two-Party Computation in the Single-Execution Setting. In Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30 - May 4, 2017, Proceedings, Part III (Lecture Notes in Computer Science), Jean-Sé bastien Coron and Jesper Buus Nielsen (Eds.), Vol. 10212. 399--424. https://doi.org/10.1007/978--3--319--56617--7_14

[68]

Xiao Wang, Samuel Ranellucci, and Jonathan Katz. 2017b. Global-Scale Secure Multiparty Computation. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, Bhavani M. Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu (Eds.). ACM, 39--56. https://doi.org/10.1145/3133956.3133979

Digital Library

[69]

Theodore M. Wong, Chenxi Wang, and Jeannette M. Wing. 2002. Verifiable Secret Redistribution for Archive System. In IEEE Security in Storage Workshop . IEEE Computer Society, 94--106.

[70]

Andrew Chi-Chih Yao. 1982. Protocols for Secure Computations (Extended Abstract). In FOCS. IEEE Computer Society, 160--164.

[71]

Lidong Zhou, Fred B. Schneider, and Robbert van Renesse. 2005. APSS: proactive secret sharing in asynchronous systems. ACM Trans. Inf. Syst. Secur., Vol. 8, 3 (2005), 259--286.

Digital Library

Cited By

Bailey BMiller ABalzarotti DXu W(2024)Formalizing soundness proofs of linear PCP SNARKsProceedings of the 33rd USENIX Conference on Security Symposium10.5555/3698900.3698984(1489-1506)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.5555/3698900.3698984
Xie XLi YZhang WWang TXu SZhu JSong Y(2024)GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00131(484-502)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00131
Dittmer SEldefrawy KGraham-Lengrand SLu SOstrovsky RPereira VMeng WJensen CCremers CKirda E(2023)Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-KnowledgeProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3616583(2098-2112)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3616583
Show More Cited By

Index Terms

A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models
    2. Logic and verification
2. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Source code generation

Recommendations

Optimizing Semi-Honest Secure Multiparty Computation for the Internet
CCS '16: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security

In the setting of secure multiparty computation, a set of parties with private inputs wish to compute some function of their inputs without revealing anything but their output. Over the last decade, the efficiency of secure two-party computation has ...
Efficient Secure Multiparty Computation with Identifiable Abort
Proceedings, Part I, of the 14th International Conference on Theory of Cryptography - Volume 9985

We study secure multiparty computation MPC in the dishonest majority setting providing security with identifiable abort, where if the protocol aborts, the honest parties can agree upon the identity of a corrupt party. All known constructions that ...
Bit Decomposition Protocols in Secure Multiparty Computation
WAHC '18: Proceedings of the 6th Workshop on Encrypted Computing & Applied Homomorphic Cryptography

We present improved protocols for the conversion of secret-shared bit-vectors into secret-shared integers and vice versa, for the use as subroutines in secure multiparty computation (SMC) protocols and for protocols verifying the adherence of parties to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '19: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security

November 2019

2755 pages

ISBN:9781450367479

DOI:10.1145/3319535

General Chairs:
Lorenzo Cavallaro
King's College London, UK
,
Johannes Kinder
Bundeswehr University Munich, Germany
,
Program Chairs:
XiaoFeng Wang
Indiana University, USA
,
Jonathan Katz
George Mason University, USA

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 November 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Fundacao para a Ciencia e Tecnologia

Conference

CCS '19

Sponsor:

SIGSAC

CCS '19: 2019 ACM SIGSAC Conference on Computer and Communications Security

November 11 - 15, 2019

London, United Kingdom

Acceptance Rates

CCS '19 Paper Acceptance Rate 149 of 934 submissions, 16%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
573
Total Downloads

Downloads (Last 12 months)29
Downloads (Last 6 weeks)2

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bailey BMiller ABalzarotti DXu W(2024)Formalizing soundness proofs of linear PCP SNARKsProceedings of the 33rd USENIX Conference on Security Symposium10.5555/3698900.3698984(1489-1506)Online publication date: 14-Aug-2024
https://dl.acm.org/doi/10.5555/3698900.3698984
Xie XLi YZhang WWang TXu SZhu JSong Y(2024)GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00131(484-502)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00131
Dittmer SEldefrawy KGraham-Lengrand SLu SOstrovsky RPereira VMeng WJensen CCremers CKirda E(2023)Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-KnowledgeProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3616583(2098-2112)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3616583
Bacelar Almeida JBarbosa MBarthe GPacheco HPereira VPortela B(2022)A formal treatment of the role of verified compilers in secure computationJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2021.100736125(100736)Online publication date: Feb-2022
https://doi.org/10.1016/j.jlamp.2021.100736
Almeida JBarbosa MCorreia MEldefrawy KGraham-Lengrand SPacheco HPereira VKim YKim JVigna GShi E(2021)Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-HeadProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security10.1145/3460120.3484771(2587-2600)Online publication date: 12-Nov-2021
https://dl.acm.org/doi/10.1145/3460120.3484771
Barbosa MBarthe GBhargavan KBlanchet BCremers CLiao KParno B(2021)SoK: Computer-Aided Cryptography2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00008(777-795)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00008

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten