In this paper, we consider encryption systems with two-out-of-two threshold decryption, where one of the parties (the client) initiates the decryption and the other one (the server) assists. Existing threshold decryption schemes disclose to the server the ciphertext that is being decrypted. We give a construction, where the identity of the ciphertext is not leaked to the server, and the client's privacy is thus preserved. While showing the security of this construction, we run into the issue of defining the security of a scheme with blindly assisted decryption. We discuss previously proposed security definitions for similar cryptographic functionalities and argue why they do not capture the expected meaning of security. We propose an ideal functionality for the encryption with server-supported blind threshold decryption in the universal composability model, carefully balancing between the meaning of privacy, and the ability to implement it. We construct a protocol and show that it is a secure implementation of the proposed functionality in the random oracle model.

We present ZK-SECREC, a domain-specific language for zero-knowledge (ZK) proofs. We focus on its type system, making the point that this is the most appropriate mechanism for tracking information flows in a statement that is meant to be proved using a zero-knowledge protocol. The appropriateness stems from the necessary distinctions between the two involved parties and between the computations made locally or on top of the protocol. The appropriateness also stems from how the types match with the major steps of typical ZK protocols, including the generation of Common Reference Strings. We compare the type system of ZK-SECREC with those of the previously proposed languages for ZK proofs and privacy-preserving computations, and show how ZK-SECREC handles certain aspects better.

Abstract The development of threshold protocols based on lattice-signature schemes has been of increasing interest in the past several years. The main research focus has been towards protocols constructed for various variants of Crystals-Dilithium, future NIST digital signature standard known as ML-DSA. In this work, we propose TOPCOAT, a two-party lattice-based signature algorithm that embodies Dilithium’s compression techniques. The aforesaid result is achieved by introducing a new hinting mechanism that allows parties to collaboratively calculate $$\textsf {HighBits}$$ HighBits . Our hinting mechanism allows public key compression similar to Dilithium. Additionally, we suggest an optimization technique to minimize number of restarts both parties need to produce a valid signature. Our approach allows to produce $$\approx 10$$ ≈ 10 KB signatures within 3 rounds of communication. We prove security of our scheme under MLWE and MSIS assumptions in ROM, and provide implementation of our proposed scheme. As additional contribution, we present vulnerabilities and inconsistencies found in Liu et al. work (Future Generation Computer Systems 2023) which aimed to construct distributed lattice-based signature protocol.

We present Centralized Attribute Collection Service (CACS), a system for storing credentials in the cloud, with satisfying privacy properties for users, and additional assurances for relying parties. The system deploys privacy-enhancing technologies to protect users’ identities and credentials presented to relying parties. At the same time, the system can vouch for the trustfulness of issuers to relying parties. The system also allows users to obtain the access logs for their credentials, enabling them to compare them against their usage. The presentation of credentials to relying parties follows the standard protocols of Mobile Driving Licence (mDL, ISO 18013-5).

Differential privacy is a privacy technique with provable guarantees which is typically achieved by introducing noise to statistics before releasing them. The level of privacy is characterized by a certain numeric parameter E > 0, where smaller E means more privacy. However, there is no common agreement on how small E should be, and the actual likelihood of data leakage for the same E may vary for different released statistics and different datasets. In this paper, we show how to relate E to the increase in the probability of attacker's success in guessing something about the private data. The attacker's goal is stated as a Boolean expression over guessing particular categorical and numerical attributes, where numeric attributes can be guessed with some precision. The paper is built upon the definition of d-privacy, which is a gencralization of E-differential privacy.

The radius-stepping algorithm is an efficient, parallelixable algorithm for finding the shortest paths in graphs. It solved the problem in Δ-Stepping algorithm, which has no known theoretical bounds fur general graphs. 1" this paper, we describe a parallel privacy-preserving method for finding SingleSource Shortest Paths (SSSP). Our optimized method is based on the Radius-Stepping algorithm. The method is implemented on iop of the Secure Multiparty Computation (SMC) Sharemiiid platform. We have reshaped the radius-stepping algorithm to work on vectors representing the graph in a SIMD manner, in order to enable a fast execution using the secret-sharing based SMC protocol set of Sharemind. The results of the real implementation show an efficient method that reduced the execution time hundreds of times iii comparison with a standard case of the privacy-preserving radius-stepping and Δ-Stepping algorithms.

Owners of data may wish to share some statistics with others, but they may be worried of privacy of the underlying data. An effective solution to this problem is to employ provable privacy techniques, such as differential privacy, to add noise to the statistics before releasing them. This protection lowers the risk of sharing sensitive data with more or less trusted data sharing partners. Unfortunately, applying differential privacy in its mathematical form requires one to fix certain numeric parameters, which involves subtle computations and expert knowledge that the data owners may lack.In this paper, we first describe a differential privacy parameter selection procedure that minimizes what lay data owners need to know. Second, we describe a user visualization and workflow that makes this procedure available for lay data owners by helping them set the level of noise appropriately to achieve a tolerable risk level. Finally, we describe a user study in which human factors professionals who were native to differential privacy were briefly trained on the concept of using differential privacy for data sharing and then used the visualization to determine an appropriate level of noise.

Abstract The meaning of differential privacy (DP) is tightly bound with the notion of distance on databases, typically defined as the number of changed rows. Considering the semantics of data, this metric may be not the most suitable one, particularly when a distance comes out as larger than the data owner desired (which would undermine privacy). In this paper, we give a mechanism to specify continuous metrics that depend on the locations and amounts of changes in a much more nuanced manner. Our metrics turn the set of databases into aBanach space. In order to construct DP information release mechanisms based on our metrics, we introducederivative sensitivity, an analogue to local sensitivity for continuous functions. We use this notion in an analysis that determines the amount of noise to be added to the result of a database query in order to obtain a certain level of differential privacy, and demonstrate that derivative sensitivity allows us to employ powerful mechanisms from calculus to perform the analysis for a variety of queries. We have implemented the analyzer and evaluated its efficiency and precision.

Pleak is a tool to capture and analyze privacy-enhanced business process models to characterize and quantify to what extent the outputs of a process leak information about its inputs. Pleak incorporates an extensible set of analysis plugins, which enable users to inspect potential leakages at multiple levels of detail.

The aim of Elliptic Curve Cryptosystems (ECC) is to achieve the same security level as RSA but with shorter key size. The basic operation in the ECC is scalar multiplication which is an expensive operation. In this paper, we focus on optimizing ECC scalar multiplication based on Non-Adjacent Form (NAF). A new algorithm is introduced that combines an Add-Subtract Scalar Multiplication Algorithm with NAF representation to accelerate the performance of the ECC calculation. Parallelizing the new algorithm shows an efficient method to calculate ECC. The proposed method has speed up the calculation up to 60% compared with the standard method.

Abstract This paper presents a generic “GMW-style” method for turning passively secure protocols into protocols secure against covert attacks, adding relatively cheap offline preprocessing and post-execution verification phases. Our construction performs best with a small number of parties, and its main benefit is the total cost of the online and the offline phases. In the preprocessing phase, each party generates and shares a sufficient amount of verified multiplication triples that will be later used to assist that party’s proof. The execution phase, after which the computed result is already available to the parties, has only negligible overhead that comes from signatures on sent messages. In the postprocessing phase, the verifiers repeat the computation of the prover in secret-shared manner, checking that they obtain the same messages that the prover sent out during execution. The verification preserves the privacy guarantees of the original protocol. It is applicable to protocols doing computations over finite rings, even if the same protocol performs its computation over several distinct rings. We apply our verification method to the Sharemind platform for secure multiparty computations (SMC), evaluate its performance and compare it to other existing SMC platforms offering security against stronger than passive attackers.

We consider how to perform privacy-preserving analyses on private data from different data providers and containing personal information of many different individuals. We combine differential privacy and secret sharing based secure multiparty computation in the same system to protect the privacy of both the data providers and the individuals. We have implemented a prototype of this combination and have found that the overhead of adding differential privacy to secure multiparty computation is small enough to be usable in practice.

Sharemind is an efficient framework for secure multiparty computations (SMC). Its efficiency is in part achieved through a large set of primitive, optimized SMC protocols that it makes available to applications built on its top. The size of this set has brought with it an issue not present in frameworks with a small number of supported operations: the set of protocols must be maintained, as new protocols are still added to it and possible optimizations for a particular sub-protocol should be propagated into larger protocols working with data of different types.

We describe an automatic analysis to check secure multi-party computation protocols against privacy leaks. The analysis is sound -- a protocol that is deemed private does not leak anything about its private inputs, even if active attacks are performed against it. Privacy against active adversaries is an essential ingredient in constructions aiming to provide security (privacy + correctness) in adversarial models of intermediate (between passive and active) strength. Using our analysis we are able to show that the protocols used by the SHAREMIND secure multi-party computation platform are actively private.

Business process matching is the activity of checking whether a given business process can interoperate with another one in a correct manner. In case the check fails, it is desirable to obtain information about how the first process can be corrected with as few modifications as possible to achieve interoperability. In case the two business processes belong to two separate enterprises that want to build a virtual enterprise, business process matching based on revealing the business processes poses a clear threat to privacy, as it may expose sensitive information about the inner operation of the enterprises. In this paper we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm in the programming language SecreC, executing on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.

Abstract In this paper, we describe efficient protocols to perform in parallel many reads and writes in private arrays according to private indices. The protocol is implemented on top of the Arithmetic Black Box (ABB) and can be freely composed to build larger privacypreserving applications. For a large class of secure multiparty computation (SMC) protocols, our technique has better practical and asymptotic performance than any previous ORAM technique that has been adapted for use in SMC. Our ORAM technique opens up a large class of parallel algorithms for adoption to run on SMC platforms. In this paper, we demonstrate how the minimum spanning tree (MST) finding algorithm by Awerbuch and Shiloach can be executed without revealing any details about the underlying graph (beside its size). The data accesses of this algorithm heavily depend on the location and weight of edges (which are private) and our ORAM technique is instrumental in their execution. Our implementation is the first-ever realization of a privacypreserving MST algorithm with sublinear round complexity.

Secure multi-party computation systems are commonly built from a small set of primitive components. The compos ability of security notions has a central role in the analysis of such systems, as it allows us to deduce security properties of complex protocols from the properties of its components. We show that the standard notions of universally compos able security are overly restrictive in this context and can lead to protocols with sub-optimal performance. As a remedy, we introduce a weaker notion of privacy that is satisfied by simpler protocols and is preserved by composition. After that we fix a passive security model and show how to convert a private protocol into a universally compos able protocol. As a result, we obtain modular security proofs without performance penalties.

This paper addresses the problem of computing the intersection of regular languages in a privacy-preserving fashion. Private set intersection has been addressed earlier in the literature, but for finite sets only. We discuss the various possibilities for solving the problem efficiently, and argue for an approach based on minimal deterministic finite automata (DFA) as a suitable, non-leaking representation of regular language intersection. We propose two different algorithms for DFA minimization in a secure multiparty computation setting, illustrating different aspects of programming based on universal composability and the constraints this sets on existing algorithms. The implementation of our algorithms is based on the programming language SECREC, executing on the SHAREMIND platform for secure multiparty computation. As one application domain we consider fusion of virtual enterprise business processes.

Bilinear pairings are powerful mathematical structures that can be used in cryptography. Their equational properties allow constructing cryptographic primitives and protocols that would be otherwise ineffective or even impossible. In formal cryptography, the protocols are expressed through term algebras and process calculi. ProVerif, one of the most successful protocol analyzers, internally converts them to Horn theories for the analysis. This approach cannot easily deal with complex equational theories. In this paper, we propose an equational theory that models bilinear pairings in formal cryptography. We also propose a reduction from the derivation problem for Horn theories modulo this equational theory to (almost) purely syntactical derivation problem for Horn theories. This derivation problem can be readily tackled by ProVerif. We have implemented our analysis and have demonstrated that it is able to handle several secure and insecure protocols based on bilinear pairings. Our approach mostly follows Kusters's and Truderung's handling of Diffie-Hellman exponentiation. The greater complexity of the theory for bilinear pairings introduces several complications, the arithmetic properties of exponentiation play a much bigger role in our reduction. Still, our approach has the same kind of generality as theirs. Similarly to their approach, we do not treat the group operations as (independent) term constructors. But we show that access to those operations will not increase the power of the adversary.

To speak about the security of information flow in programs employing cryptographic operations, definitions based on computational indistinguish ability of distributions over program states have to be used. These definitions, as well as the accompanying analysis tools, are complex and error-prone to argue about. Cryptographically masked flows, proposed by Askarov, Hedin and Sabelfeld, are an abstract execution model and security definition that attempt to abstract away the details of computational security. This abstract model is useful because analysis of programs can be conducted using the usual techniques for enforcing non-interference.

We present a novel approach for proving secrecy properties of security protocols by mechanized flow analysis. In contrast to existing tools for proving secrecy by abstract interpretation, our tool enjoys cryptographic soundness in the strong sense of blackbox reactive simulatability/UC which entails that secrecy properties proven by our tool are automatically guaranteed to hold for secure cryptographic implementations of the analyzed protocol, with respect to the more fine-grained cryptographic secrecy definitions and adversary models.Our tool is capable of reasoning about a comprehensive language for expressing protocols, in particular handling symmetric encryption and asymmetric encryption, and it produces proofs for an unbounded number of sessions in the presence of an active adversary. We have implemented the tool and applied it to a number of common protocols from the literature.

We present a type system for checking secrecy of messages handled by protocols that use the Backes-Pfitzmann-Waidner library for cryptographic operations. A secure realization of this library exists, therefore we obtain for the first time a cryptographically sound analysis for a full language for expressing protocols, particularly handling symmetric encryption and unbounded number of sessions. The language is similar to the spi-calculus, but has a completely deterministic semantics. The type system is similar to the Abadi-Blanchet type system for asymmetric communication.

In this article we present a technique for static analysis, correct with respect to complexity-theoretic definitions of security, of cryptographic protocols for checking whether these protocols satisfy confidentiality properties. The approach is similar to Abadi and Rogaway - we define patterns for cryptographic protocols (they did it for formal expressions), such that the protocol is secure iff the patterns are. We then statically analyse the patterns, they should be easier to analyse than the protocols themselves. We consider symmetric encryption as the cryptographic primitive in protocols. Handling this primitive has so far received comparatively less attention in approaches striving to unite the formal and computational models of cryptography.

This paper presents a method to increase the accountability of certificate management by making it intractable for the certification authority (CA) to create contradictory statements about the validity of a certificate. The core of the method is a new primitive, undeniable attester, that allows som eone to commit to some set S of bitstrings by publishing a short digest of S and to give attestations for any x that it is or is not a member of S. Such an attestation can be verified by obtaining in authenticated way the published digest and applying a verification algorithm to the triple of the bitstring, the attestation and the digest. The most important feature of this primitive is intractability of creating two contradictory proofs for the same candidate element x and digest. We give an efficient construction for undeniable attesters based on authenticated search trees. We show that the construction also applies to sets of more structured elements. We also show that undeniable attesters exist iff collision-resistant hash functions exist.

This paper initiates a study of accountable certificate management methods, necessary to support long-term authenticity of digital documents.Our main contribution is a model for accountable certificate management, where clients receive attestations confirming inclusion/removal of their certificates from the database of valid certificates.We explain why accountability depends on the inability of the third parties to create contradictory attestations.After that we define an undeniable attester as a primitive that provides efficient attestation creation, publishing and verification, so that it is intractable to create contradictory attestations.We introduce authenticated search trees and build an efficient undeniable attester upon them.The proposed system is the first accountable long-term certificate management system.Moreover, authenticated search trees can be used in many security-critical applications instead of the (sorted) hash trees to reduce trust in the authorities, without decrease in efficiency.Therefore, the undeniable attester promises looks like a very useful cryptographic primitive with a wide range of applications.