Florian Kammueller, Manfred Kerber, Christian W. Probst
This paper applies machine assisted formal methods to explore insider threats for auctions. Auction systems, like eBay, are an important problem domain for formal analysis because they challenge modelling concepts as well as analysis methods. We use machine assisted formal modelling and proof in Isabelle to demonstrate how security and privacy goals of auction protocols can be formally verified. Applying the costly scrutiny of formal methods is justified for auctions since privacy and trust are prominent issues and auctions are sometimes designed for one-off occasions where high bids are at stake. For example, when radio wave frequencies are on sale, auctions are especially created for just one occasion where fair and consistent behaviour is required. Investigating the threats in auctions and insider collusions, we model and analyze auction protocols for insider threats using the interactive theorem prover Isabelle. We use the existing example of a fictitious cocaine auction protocol from the literature to develop and illustrate our approach. Combining the Isabelle Insider framework with the inductive approach to verifying security protocols in Isabelle, we formalize the cocaine auction protocol, prove that this formal definition excludes sweetheart deals, and also that collusion attacks cannot generally be excluded. The practical implication of the formalization is demonstrated by code generation. Isabelle allows generating code from constructive specifications into the programming language Scala. We provide constructive test functions for cocaine auction traces, prove within Isabelle that these functions conform to the protocol definition, and apply code generation to produce an implementation of the executable test predicate for cocaine auction traces in Scala.
Andrew Miller, Iddo Bentov, Surya Bakshi, Ranjit Kumaresan · 5 authors
Bitcoin, Ethereum and other blockchain-based cryptocurrencies, as deployed today, cannot scale for wide-spread use. A leading approach for cryptocurrency scaling is a smart contract mechanism called a payment channel which enables two mutually distrustful parties to transact efficiently (and only requires a single transaction in the blockchain to set-up). Payment channels can be linked together to form a payment network, such that payments between any two parties can (usually) be routed through the network along a path that connects them. Crucially, both parties can transact without trusting hops along the route. In this paper, we propose a novel variant of payment channels, called Sprites, that reduces the worst-case "collateral cost" that each hop along the route may incur. The benefits of Sprites are two-fold. 1) In Lightning Network, a payment across a path of $\ell$ channels requires locking up collateral for $Θ(\ellΔ)$ time, where $Δ$ is the time to commit an on-chain transaction. Sprites reduces this cost to $O(\ell + Δ)$. 2) Unlike prior work, Sprites supports partial withdrawals and deposits, during which the channel can continue to operate without interruption. In evaluating Sprites we make several additional contributions. First, our simulation-based security model is the first formalism to model timing guarantees in payment channels. Our construction is also modular, making use of a generic abstraction from folklore, called the "state channel," which we are the first to formalize. We also provide a simulation framework for payment network protocols, which we use to confirm that the Sprites construction mitigates against throughput-reducing attacks.
Thomas Dickerson, Paul Gazzillo, Maurice Herlihy, Eric Koskinen
Modern cryptocurrency systems, such as Ethereum, permit complex financial transactions through scripts called smart contracts. These smart contracts are executed many, many times, always without real concurrency. First, all smart contracts are serially executed by miners before appending them to the blockchain. Later, those contracts are serially re-executed by validators to verify that the smart contracts were executed correctly by miners. Serial execution limits system throughput and fails to exploit today's concurrent multicore and cluster architectures. Nevertheless, serial execution appears to be required: contracts share state, and contract programming languages have a serial semantics. This paper presents a novel way to permit miners and validators to execute smart contracts in parallel, based on techniques adapted from software transactional memory. Miners execute smart contracts speculatively in parallel, allowing non-conflicting contracts to proceed concurrently, and "discovering" a serializable concurrent schedule for a block's transactions, This schedule is captured and encoded as a deterministic fork-join program used by validators to re-execute the miner's parallel schedule deterministically but concurrently. Smart contract benchmarks run on a JVM with ScalaSTM show that a speedup of of 1.33x can be obtained for miners and 1.69x for validators with just three concurrent threads.
This paper analyses the Bitcoin system and attempts to split the production costs and the market valorization. This analysis is performed from public data and technical research papers. We introduce the design of secure elements dedicated to Bitcoin transactions. Such devices will available trusted and fast transactions, and should avoid Bitcoin address hijacking.
Data is nowadays an invaluable resource, indeed it guides all business decisions in most of the computer-aided human activities. Threats to data integrity are thus of paramount relevance, as tampering with data may maliciously affect crucial business decisions. This issue is especially true in cloud computing environments, where data owners cannot control fundamental data aspects, like the physical storage of data and the control of its accesses. Blockchain has recently emerged as a fascinating technology<br> which, among others, provides compelling properties about data integrity. Using the blockchain to face data integrity threats seems to be a natural choice, but its current limitations of low throughput, high latency, and weak stability hinder the practical feasibility of any blockchain-based solutions.<br> In this paper, by focusing on a case study from the European SUNFISH project, which concerns the design of a secure by-design cloud federation platform for the public sector, we precisely delineate the actual data integrity needs of cloud computing environments and the research questions to be tackled to adopt blockchain-based databases. First, we detail the open research questions and the difficulties inherent in addressing them. Then, we outline a preliminary design of an effective blockchain-based database for cloud computing environments.
With the emergence of Bitcoin, businesses are focusing on leveraging Bitcoin's blockchain technology to non-cryptocurrency based applications to improve efficiency of the operations. These business applications operate in environments where participants have verified identities; these are called permissioned environments. Blockchain is an immutable and append only distributed ledger that can be utilized for record keeping applications. We observe that when blockchain technology is adapted from permissionless environments to permissioned environments the immutability of blockchain becomes questionable as the end-users may not monitor or store a copy of the blockchain. We propose the use of Keyless Signatures' Infrastructure as an additional mechanism to ensure irreversible and irrefutable proof of block confirmations which acts as a global proof thus preserving long term immutability of blockchain in permissioned environments.
Blockchain Technology Applications and Security
Cryptography and Data Security
Advanced Steganography and Watermarking Techniques
In this paper a novel feedback controller and stability analysis of a blockchain implementation is developed by using a control engineering perspective. The controller output equals the difficulty adjustment in the mining process while the feedback variable is the average block time over a certain time period. The computational power (hash rate) of the miners is considered a disturbance in the model. The developed controller is tested against a simulation model with constant disturbance, step and ramp responses as well as with a high-frequency sinusoidal disturbance. Stability and a fast response is demonstrated in all these cases with a controller which adjusts it's output at every new block. Finally the performance of the controller is implemented and demonstrated on a testnet with a constant hash rate as well as on the mainnet of a public open source blockchain project.
Decentralized trusted timestamping based on blockchains is used to protect a large variety of digital data. At present, in the case of trusted timestamping services, such related information is not included in the OP_RETURN field of a Bitcoin's transaction chain, which has a limited size (40 bytes). When OP_RETURN is extended, (e.g., with multiple OP_RETURN fields) the transaction is rejected by the Bitcoin network. We propose storing data in the blockchain by encoding into Bitcoin addresses. The transactions created by the proposed method are similar to the usual transactions; therefore, they will not be rejected. The proposed method expands the storage space to a maximum of N*20 bytes, thereby enabling the storage of additional information (e.g., file names, creator names, and keywords) as well as file hashes. We performed experiments with a picture and its copyright information. We set N =3, resulting in storage of 60 bytes of data. The experimental results indicate that the proposed method can timestamp a file in an average of 24 min at a possible cost of 0.24 USD. We believe that the proposed method can prove the existence and integrity of a digital file, which is helpful in copyright protection.
Secure multiparty protocols are useful tools for parties wishing to jointly compute a function while keeping their input data secret. The millionaires’ problem is the first secure two-party computation problem, where the goal is to securely compare two private numbers without a trusted third-party. There have been several solutions to the problem, including Yao’s protocol [Yao, 1982] and Mix and Match [Jakobsson and Juels, 2000]. However, Yao’s Protocol is not secure in the malicious model and Mix and Match unnecessarily releases theoretically breakable encryptions of information about the data that is not needed for the comparison. In addition, neither protocol has any verification of the validity of the inputs before they are used. In this thesis, we introduce Variance, a privacy-preserving two-party protocol for solving the Yao’s millionaires’ problem in a Bitcoin setting, in which each party controls several Bitcoin accounts (public Bitcoin addresses) and they want to find out who owns more bitcoins without revealing (1) how many accounts they own and the balance of each account, (2) the addresses associated with their accounts, and (3) their total wealth of bitcoins while assuring the other party that they are not claiming more bitcoin than they possess. We utilize commitments, encryptions, zero knowledge proofs, and homomorphisms as the major computational tools to provide a solution to the problem, and subsequently prove that the solution is secure against active adversaries in the malicious model.
Low-power Ad Hoc systems are the most challenging aspect for secured Ad Hoc systems. The resource constrained devices were easily tampered due to the limited operated environment. Over the past decade, the usage rate of Ad Hoc systems are rapidly increased in modern communication systems. However, the security is still a research factor for Lowpower Ad Hoc systems. Offering Security and Anonymity is an important research issue in Low-power Mobile Ad Hoc Networks (LPMANET). Various anonymous routing protocols presented to maintain anonymity in adverse environment, these protocols proven significant results in Ad Hoc systems but failure to improved the anonymity efficiency in Low-power Ad hoc networks. In this paper, a Lightweight Energy Efficient Anonymous Routing (LEEAR) protocol is proposed to offer energy efficient anonymity and security in an adverse environment by combining modified zero knowledge proof, bloom filter and cryptography techniques. We designed the LEEAR protocol to determine the efficiency in-terms security and energy against routing level and traffic level attacks. We simulated the experiment in NS2 simulator the determine the results and ensure importance of the proposed LEEAR protocol in accomplishing energy efficiency and anonymity.
We demonstrate that the Bitcoin Script language allows not only for primitive recursion, but in the deployment of an Ackerman function and hence the ability to simply recurse in Bitcoin script, we show that the script system is Turing complete. From this, we introduce a new class of Turing Machine, the PTTM or probabilistic Total Turing machine and note that Bitcoin acts as a decider or Total Turing Machine which allows us to find a NIZKPoK that can act as a TM based verifier to a Non-Interactive Proof that is run on an external and non-associated TM as a proof system. Bitcoin can extend to securely offer contracts such as best fit solutions to common logistic systems and optimisation problems including the Travelling Salesman class of problems and to the optimisation of systems. This can be offered as an open or time bound contract that guarantees payment and can be solved which allowing Pseudonymity of the bidder.