TY - CONF
AB - Yao’s garbling scheme is one of the most fundamental cryptographic constructions. Lindell and Pinkas (Journal of Cryptograhy 2009) gave a formal proof of security in the selective setting where the adversary chooses the challenge inputs before seeing the garbled circuit assuming secure symmetric-key encryption (and hence one-way functions). This was followed by results, both positive and negative, concerning its security in the, stronger, adaptive setting. Applebaum et al. (Crypto 2013) showed that it cannot satisfy adaptive security as is, due to a simple incompressibility argument. Jafargholi and Wichs (TCC 2017) considered a natural adaptation of Yao’s scheme (where the output mapping is sent in the online phase, together with the garbled input) that circumvents this negative result, and proved that it is adaptively secure, at least for shallow circuits. In particular, they showed that for the class of circuits of depth δ , the loss in security is at most exponential in δ . The above results all concern the simulation-based notion of security. In this work, we show that the upper bound of Jafargholi and Wichs is basically optimal in a strong sense. As our main result, we show that there exists a family of Boolean circuits, one for each depth δ∈N , such that any black-box reduction proving the adaptive indistinguishability of the natural adaptation of Yao’s scheme from any symmetric-key encryption has to lose a factor that is exponential in δ√ . Since indistinguishability is a weaker notion than simulation, our bound also applies to adaptive simulation. To establish our results, we build on the recent approach of Kamath et al. (Eprint 2021), which uses pebbling lower bounds in conjunction with oracle separations to prove fine-grained lower bounds on loss in cryptographic security.
AU - Kamath Hosdurg, Chethan
AU - Klein, Karen
AU - Pietrzak, Krzysztof Z
AU - Wichs, Daniel
ID - 10041
SN - 0302-9743
T2 - 41st Annual International Cryptology Conference, Part II
TI - Limits on the Adaptive Security of Yao’s Garbling
VL - 12826
ER -
TY - CONF
AB - For 1≤m≤n, we consider a natural m-out-of-n multi-instance scenario for a public-key encryption (PKE) scheme. An adversary, given n independent instances of PKE, wins if he breaks at least m out of the n instances. In this work, we are interested in the scaling factor of PKE schemes, SF, which measures how well the difficulty of breaking m out of the n instances scales in m. That is, a scaling factor SF=ℓ indicates that breaking m out of n instances is at least ℓ times more difficult than breaking one single instance. A PKE scheme with small scaling factor hence provides an ideal target for mass surveillance. In fact, the Logjam attack (CCS 2015) implicitly exploited, among other things, an almost constant scaling factor of ElGamal over finite fields (with shared group parameters).
For Hashed ElGamal over elliptic curves, we use the generic group model to argue that the scaling factor depends on the scheme's granularity. In low granularity, meaning each public key contains its independent group parameter, the scheme has optimal scaling factor SF=m; In medium and high granularity, meaning all public keys share the same group parameter, the scheme still has a reasonable scaling factor SF=√m. Our findings underline that instantiating ElGamal over elliptic curves should be preferred to finite fields in a multi-instance scenario.
As our main technical contribution, we derive new generic-group lower bounds of Ω(√(mp)) on the difficulty of solving both the m-out-of-n Gap Discrete Logarithm and the m-out-of-n Gap Computational Diffie-Hellman problem over groups of prime order p, extending a recent result by Yun (EUROCRYPT 2015). We establish the lower bound by studying the hardness of a related computational problem which we call the search-by-hypersurface problem.
AU - Auerbach, Benedikt
AU - Giacon, Federico
AU - Kiltz, Eike
ID - 7966
SN - 0302-9743
T2 - Advances in Cryptology – EUROCRYPT 2020
TI - Everybody’s a target: Scalability in public-key encryption
VL - 12107
ER -
TY - CONF
AB - This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the Civl verifier.
AU - Kragl, Bernhard
AU - Qadeer, Shaz
AU - Henzinger, Thomas A
ID - 8195
SN - 0302-9743
T2 - Computer Aided Verification
TI - Refinement for structured concurrent programs
VL - 12224
ER -
TY - CONF
AB - We introduce the monitoring of trace properties under assumptions. An assumption limits the space of possible traces that the monitor may encounter. An assumption may result from knowledge about the system that is being monitored, about the environment, or about another, connected monitor. We define monitorability under assumptions and study its theoretical properties. In particular, we show that for every assumption A, the boolean combinations of properties that are safe or co-safe relative to A are monitorable under A. We give several examples and constructions on how an assumption can make a non-monitorable property monitorable, and how an assumption can make a monitorable property monitorable with fewer resources, such as integer registers.
AU - Henzinger, Thomas A
AU - Sarac, Naci E
ID - 8623
SN - 0302-9743
T2 - Runtime Verification
TI - Monitorability under assumptions
VL - 12399
ER -
TY - CONF
AB - A simple drawing D(G) of a graph G is one where each pair of edges share at most one point: either a common endpoint or a proper crossing. An edge e in the complement of G can be inserted into D(G) if there exists a simple drawing of G+e extending D(G). As a result of Levi’s Enlargement Lemma, if a drawing is rectilinear (pseudolinear), that is, the edges can be extended into an arrangement of lines (pseudolines), then any edge in the complement of G can be inserted. In contrast, we show that it is NP -complete to decide whether one edge can be inserted into a simple drawing. This remains true even if we assume that the drawing is pseudocircular, that is, the edges can be extended to an arrangement of pseudocircles. On the positive side, we show that, given an arrangement of pseudocircles A and a pseudosegment σ , it can be decided in polynomial time whether there exists a pseudocircle Φσ extending σ for which A∪{Φσ} is again an arrangement of pseudocircles.
AU - Arroyo Guevara, Alan M
AU - Klute, Fabian
AU - Parada, Irene
AU - Seidel, Raimund
AU - Vogtenhuber, Birgit
AU - Wiedera, Tilo
ID - 8732
SN - 0302-9743
T2 - Graph-Theoretic Concepts in Computer Science
TI - Inserting one edge into a simple drawing is hard
VL - 12301
ER -
TY - CONF
AB - Discrete-time Markov Chains (MCs) and Markov Decision Processes (MDPs) are two standard formalisms in system analysis. Their main associated quantitative objectives are hitting probabilities, discounted sum, and mean payoff. Although there are many techniques for computing these objectives in general MCs/MDPs, they have not been thoroughly studied in terms of parameterized algorithms, particularly when treewidth is used as the parameter. This is in sharp contrast to qualitative objectives for MCs, MDPs and graph games, for which treewidth-based algorithms yield significant complexity improvements. In this work, we show that treewidth can also be used to obtain faster algorithms for the quantitative problems. For an MC with n states and m transitions, we show that each of the classical quantitative objectives can be computed in O((n+m)⋅t2) time, given a tree decomposition of the MC with width t. Our results also imply a bound of O(κ⋅(n+m)⋅t2) for each objective on MDPs, where κ is the number of strategy-iteration refinements required for the given input and objective. Finally, we make an experimental evaluation of our new algorithms on low-treewidth MCs and MDPs obtained from the DaCapo benchmark suite. Our experiments show that on low-treewidth MCs and MDPs, our algorithms outperform existing well-established methods by one or more orders of magnitude.
AU - Asadi, Ali
AU - Chatterjee, Krishnendu
AU - Goharshady, Amir Kafshdar
AU - Mohammadi, Kiarash
AU - Pavlogiannis, Andreas
ID - 8728
SN - 0302-9743
T2 - Automated Technology for Verification and Analysis
TI - Faster algorithms for quantitative analysis of MCs and MDPs with small treewidth
VL - 12302
ER -
TY - CONF
AB - Proofs of sequential work (PoSW) are proof systems where a prover, upon receiving a statement χ and a time parameter T computes a proof ϕ(χ,T) which is efficiently and publicly verifiable. The proof can be computed in T sequential steps, but not much less, even by a malicious party having large parallelism. A PoSW thus serves as a proof that T units of time have passed since χ
was received.
PoSW were introduced by Mahmoody, Moran and Vadhan [MMV11], a simple and practical construction was only recently proposed by Cohen and Pietrzak [CP18].
In this work we construct a new simple PoSW in the random permutation model which is almost as simple and efficient as [CP18] but conceptually very different. Whereas the structure underlying [CP18] is a hash tree, our construction is based on skip lists and has the interesting property that computing the PoSW is a reversible computation.
The fact that the construction is reversible can potentially be used for new applications like constructing proofs of replication. We also show how to “embed” the sloth function of Lenstra and Weselowski [LW17] into our PoSW to get a PoSW where one additionally can verify correctness of the output much more efficiently than recomputing it (though recent constructions of “verifiable delay functions” subsume most of the applications this construction was aiming at).
AU - Abusalah, Hamza M
AU - Kamath Hosdurg, Chethan
AU - Klein, Karen
AU - Pietrzak, Krzysztof Z
AU - Walter, Michael
ID - 7411
SN - 0302-9743
T2 - Advances in Cryptology – EUROCRYPT 2019
TI - Reversible proofs of sequential work
VL - 11477
ER -
TY - CHAP
AB - We illustrate the ingredients of the state-of-the-art of model-based approach for the formal design and verification of cyber-physical systems. To capture the interaction between a discrete controller and its continuously evolving environment, we use the formal models of timed and hybrid automata. We explain the steps of modeling and verification in the tools Uppaal and SpaceEx using a case study based on a dual-chamber implantable pacemaker monitoring a human heart. We show how to design a model as a composition of components, how to construct models at varying levels of detail, how to establish that one model is an abstraction of another, how to specify correctness requirements using temporal logic, and how to verify that a model satisfies a logical requirement.
AU - Alur, Rajeev
AU - Giacobbe, Mirco
AU - Henzinger, Thomas A
AU - Larsen, Kim G.
AU - Mikučionis, Marius
ED - Steffen, Bernhard
ED - Woeginger, Gerhard
ID - 7453
SN - 0302-9743
T2 - Computing and Software Science
TI - Continuous-time models for system design and analysis
VL - 10000
ER -
TY - CONF
AB - We propose a new non-orthogonal basis to express the 3D Euclidean space in terms of a regular grid. Every grid point, each represented by integer 3-coordinates, corresponds to rhombic dodecahedron centroid. Rhombic dodecahedron is a space filling polyhedron which represents the close packing of spheres in 3D space and the Voronoi structures of the face centered cubic (FCC) lattice. In order to illustrate the interest of the new coordinate system, we propose the characterization of 3D digital plane with its topological features, such as the interrelation between the thickness of the digital plane and the separability constraint we aim to obtain. A characterization of a 3D digital sphere with relevant topological features is proposed as well with the help of a 48 symmetry that comes with the new coordinate system.
AU - Biswas, Ranita
AU - Largeteau-Skapin, Gaëlle
AU - Zrour, Rita
AU - Andres, Eric
ID - 6163
SN - 0302-9743
T2 - Lecture Notes in Computer Science
TI - Rhombic dodecahedron grid—coordinate system and 3D digital object definitions
VL - 11414
ER -
TY - CONF
AB - Computer vision systems for automatic image categorization have become accurate and reliable enough that they can run continuously for days or even years as components of real-world commercial applications. A major open problem in this context, however, is quality control. Good classification performance can only be expected if systems run under the specific conditions, in particular data distributions, that they were trained for. Surprisingly, none of the currently used deep network architectures have a built-in functionality that could detect if a network operates on data from a distribution it was not trained for, such that potentially a warning to the human users could be triggered. In this work, we describe KS(conf), a procedure for detecting such outside of specifications (out-of-specs) operation, based on statistical testing of the network outputs. We show by extensive experiments using the ImageNet, AwA2 and DAVIS datasets on a variety of ConvNets architectures that KS(conf) reliably detects out-of-specs situations. It furthermore has a number of properties that make it a promising candidate for practical deployment: it is easy to implement, adds almost no overhead to the system, works with all networks, including pretrained ones, and requires no a priori knowledge of how the data distribution could change.
AU - Sun, Rémy
AU - Lampert, Christoph
ID - 6482
SN - 0302-9743
TI - KS(conf): A light-weight test if a ConvNet operates outside of Its specifications
VL - 11269
ER -
TY - CHAP
AB - Randomness is an essential part of any secure cryptosystem, but many constructions rely on distributions that are not uniform. This is particularly true for lattice based cryptosystems, which more often than not make use of discrete Gaussian distributions over the integers. For practical purposes it is crucial to evaluate the impact that approximation errors have on the security of a scheme to provide the best possible trade-off between security and performance. Recent years have seen surprising results allowing to use relatively low precision while maintaining high levels of security. A key insight in these results is that sampling a distribution with low relative error can provide very strong security guarantees. Since floating point numbers provide guarantees on the relative approximation error, they seem a suitable tool in this setting, but it is not obvious which sampling algorithms can actually profit from them. While previous works have shown that inversion sampling can be adapted to provide a low relative error (Pöppelmann et al., CHES 2014; Prest, ASIACRYPT 2017), other works have called into question if this is possible for other sampling techniques (Zheng et al., Eprint report 2018/309). In this work, we consider all sampling algorithms that are popular in the cryptographic setting and analyze the relationship of floating point precision and the resulting relative error. We show that all of the algorithms either natively achieve a low relative error or can be adapted to do so.
AU - Walter, Michael
ED - Buchmann, J
ED - Nitaj, A
ED - Rachidi, T
ID - 6726
SN - 0302-9743
T2 - Progress in Cryptology – AFRICACRYPT 2019
TI - Sampling the integers with low relative error
VL - 11627
ER -
TY - CONF
AB - Sharding, or partitioning the system’s state so that different subsets of participants handle it, is a proven approach to building distributed systems whose total capacity scales horizontally with the number of participants. Many distributed ledgers have adopted this approach to increase their performance, however, they focus on the permissionless setting that assumes the existence of a strong adversary. In this paper, we deploy channels for permissioned blockchains. Our first contribution is to adapt sharding on asset-management applications for the permissioned setting, while preserving liveness and safety even on transactions spanning across-channels. Our second contribution is to leverage channels as a confidentiality boundary, enabling different organizations and consortia to preserve their privacy within their channels and still be part of a bigger collaborative ecosystem. To make our system concrete we map it on top of Hyperledger Fabric.
AU - Androulaki, Elli
AU - Cachin, Christian
AU - De Caro, Angelo
AU - Kokoris Kogias, Eleftherios
ID - 8298
SN - 0302-9743
T2 - Computer Security
TI - Channels: Horizontal scaling and confidentiality on permissioned blockchains
VL - 11098
ER -
TY - CONF
AB - In this paper, we propose an algorithm to build discrete spherical shell having integer center and real-valued inner and outer radii on the face-centered cubic (FCC) grid. We address the problem by mapping it to a 2D scenario and building the shell layer by layer on hexagonal grids with additive manufacturing in mind. The layered hexagonal grids get shifted according to need as we move from one layer to another and forms the FCC grid in 3D. However, we restrict our computation strictly to 2D in order to utilize symmetry and simplicity.
AU - Koshti, Girish
AU - Biswas, Ranita
AU - Largeteau-Skapin, Gaëlle
AU - Zrour, Rita
AU - Andres, Eric
AU - Bhowmick, Partha
ID - 6164
SN - 0302-9743
T2 - Lecture Notes in Computer Science
TI - Sphere construction on the FCC grid interpreted as layered hexagonal grids in 3D
VL - 11255
ER -
TY - CONF
AB - Bitcoin has become the most successful cryptocurrency ever deployed, and its most distinctive feature is that it is decentralized. Its underlying protocol (Nakamoto consensus) achieves this by using proof of work, which has the drawback that it causes the consumption of vast amounts of energy to maintain the ledger. Moreover, Bitcoin mining dynamics have become less distributed over time.
Towards addressing these issues, we propose SpaceMint, a cryptocurrency based on proofs of space instead of proofs of work. Miners in SpaceMint dedicate disk space rather than computation. We argue that SpaceMint’s design solves or alleviates several of Bitcoin’s issues: most notably, its large energy consumption. SpaceMint also rewards smaller miners fairly according to their contribution to the network, thus incentivizing more distributed participation.
This paper adapts proof of space to enable its use in cryptocurrency, studies the attacks that can arise against a Bitcoin-like blockchain that uses proof of space, and proposes a new blockchain format and transaction types to address these attacks. Our prototype shows that initializing 1 TB for mining takes about a day (a one-off setup cost), and miners spend on average just a fraction of a second per block mined. Finally, we provide a game-theoretic analysis modeling SpaceMint as an extensive game (the canonical game-theoretic notion for games that take place over time) and show that this stylized game satisfies a strong equilibrium notion, thereby arguing for SpaceMint ’s stability and consensus.
AU - Park, Sunoo
AU - Kwon, Albert
AU - Fuchsbauer, Georg
AU - Gazi, Peter
AU - Alwen, Joel F
AU - Pietrzak, Krzysztof Z
ID - 6941
SN - 0302-9743
T2 - 22nd International Conference on Financial Cryptography and Data Security
TI - SpaceMint: A cryptocurrency based on proofs of space
VL - 10957
ER -
TY - CONF
AB - Space filling circles and spheres have various applications in mathematical imaging and physical modeling. In this paper, we first show how the thinnest (i.e., 2-minimal) model of digital sphere can be augmented to a space filling model by fixing certain “simple voxels” and “filler voxels” associated with it. Based on elementary number-theoretic properties of such voxels, we design an efficient incremental algorithm for generation of these space filling spheres with successively increasing radius. The novelty of the proposed technique is established further through circular space filling on 3D digital plane. As evident from a preliminary set of experimental result, this can particularly be useful for parallel computing of 3D Voronoi diagrams in the digital space.
AU - Dwivedi, Shivam
AU - Gupta, Aniket
AU - Roy, Siddhant
AU - Biswas, Ranita
AU - Bhowmick, Partha
ID - 5801
SN - 0302-9743
TI - Fast and Efficient Incremental Algorithms for Circular and Spherical Propagation in Integer Space
VL - 10502
ER -
TY - CONF
AB - This papers introduces a definition of digital primitives based on focal points and weighted distances (with positive weights). The proposed definition is applicable to general dimensions and covers in its gamut various regular curves and surfaces like circles, ellipses, digital spheres and hyperspheres, ellipsoids and k-ellipsoids, Cartesian k-ovals, etc. Several interesting properties are presented for this class of digital primitives such as space partitioning, topological separation, and connectivity properties. To demonstrate further the potential of this new way of defining digital primitives, we propose, as extension, another class of digital conics defined by focus-directrix combination.
AU - Andres, Eric
AU - Biswas, Ranita
AU - Bhowmick, Partha
ID - 5802
SN - 0302-9743
TI - Digital Primitives Defined by Weighted Focal Set
VL - 10502
ER -
TY - CHAP
AB - Different distance metrics produce Voronoi diagrams with different properties. It is a well-known that on the (real) 2D plane or even on any 3D plane, a Voronoi diagram (VD) based on the Euclidean distance metric produces convex Voronoi regions. In this paper, we first show that this metric produces a persistent VD on the 2D digital plane, as it comprises digitally convex Voronoi regions and hence correctly approximates the corresponding VD on the 2D real plane. Next, we show that on a 3D digital plane D, the Euclidean metric spanning over its voxel set does not guarantee a digital VD which is persistent with the real-space VD. As a solution, we introduce a novel concept of functional-plane-convexity, which is ensured by the Euclidean metric spanning over the pedal set of D. Necessary proofs and some visual result have been provided to adjudge the merit and usefulness of the proposed concept.
AU - Biswas, Ranita
AU - Bhowmick, Partha
ID - 5803
SN - 0302-9743
T2 - Combinatorial image analysis
TI - Construction of Persistent Voronoi Diagram on 3D Digital Plane
VL - 10256
ER -
TY - CHAP
AU - Sen, Nabhasmita
AU - Biswas, Ranita
AU - Bhowmick, Partha
ID - 5805
SN - 0302-9743
T2 - Computational Topology in Image Context
TI - On Some Local Topological Properties of Naive Discrete Sphere
VL - 9667
ER -
TY - CONF
AB - Although the concept of functional plane for naive plane is studied and reported in the literature in great detail, no similar study is yet found for naive sphere. This article exposes the first study in this line, opening up further prospects of analyzing the topological properties of sphere in the discrete space. We show that each quadraginta octant Q of a naive sphere forms a bijection with its projected pixel set on a unique coordinate plane, which thereby serves as the functional plane of Q, and hence gives rise to merely mono-jumps during back projection. The other two coordinate planes serve as para-functional and dia-functional planes for Q, as the former is ‘mono-jumping’ but not bijective, whereas the latter holds neither of the two. Owing to this, the quadraginta octants form symmetry groups and subgroups with equivalent jump conditions. We also show a potential application in generating a special class of discrete 3D circles based on back projection and jump bridging by Steiner voxels. A circle in this class possesses 4-symmetry, uniqueness, and bounded distance from the underlying real sphere and real plane.
AU - Biswas, Ranita
AU - Bhowmick, Partha
ID - 5806
SN - 0302-9743
T2 - Discrete Geometry for Computer Imagery
TI - On Functionality of Quadraginta Octants of Naive Sphere with Application to Circle Drawing
VL - 9647
ER -
TY - CHAP
AB - A discrete spherical circle is a topologically well-connected 3D circle in the integer space, which belongs to a discrete sphere as well as a discrete plane. It is one of the most important 3D geometric primitives, but has not possibly yet been studied up to its merit. This paper is a maiden exposition of some of its elementary properties, which indicates a sense of its profound theoretical prospects in the framework of digital geometry. We have shown how different types of discretization can lead to forbidden and admissible classes, when one attempts to define the discretization of a spherical circle in terms of intersection between a discrete sphere and a discrete plane. Several fundamental theoretical results have been presented, the algorithm for construction of discrete spherical circles has been discussed, and some test results have been furnished to demonstrate its practicality and usefulness.
AU - Biswas, Ranita
AU - Bhowmick, Partha
AU - Brimkov, Valentin E.
ID - 5809
SN - 0302-9743
T2 - Combinatorial image analysis
TI - On the Connectivity and Smoothness of Discrete Spherical Circles
VL - 9448
ER -