Search

Participatory sensing is often used in environmental or personal data monitoring, wherein a number of participants collect data using their mobile intelligent devices for earning the incentives. However, a lot of additional information is submitted along with the data, such as the participant’s location, IP and incentives. This multimodal information implicitly links to the participant’s identity and exposes the participant’s privacy. In order to solve the issue of these multimodal information associating with participants’ identities, this paper proposes a protocol to ensure anonymous data reporting while providing a dynamic incentive mechanism simultaneously. The proposed protocol first establishes a submission schedule by anonymously selecting a slot in a vector by each member where every member and system entities are oblivious of other members’ slots and then uses this schedule to submit the all members’ data in an encoded vector through bulk transfer and multiplayer dining cryptographers networks (DC-nets) . Hence, the link between the data and the member’s identity is broken. The incentive mechanism uses blind signature to anonymously mark the price and complete the micropayments transfer. Finally, the theoretical analysis of the protocol proves the anonymity, integrity, and efficiency of this protocol. We implemented and tested the protocol on Android phones. The experiment results show that the protocol is efficient for low latency tolerable applications, which is the cases with most participatory sensing applications, and they also show the advantage of our optimization over similar anonymous data reporting protocols.

A k-anonymous broadcast can be implemented using a small group of dining cryptographers to first share the message, followed by a flooding phase started by group members. Members have little incentive to forward the message in a timely manner, as forwarding incurs costs, or they may even profit from keeping the message. In worst case, this leaves the true originator as the only sender, rendering the dining-cryptographers phase useless and compromising their privacy. We present a novel approach using a modified dining-cryptographers protocol to distributed shares of an (n,k)-Shamir's secret sharing scheme. Finally, all group members broadcast their received share through the network, allowing any recipient of k shares to reconstruct the message, enforcing anonymity. If less than k group members broadcast their shares, the message cannot be decoded thus preventing privacy breaches for the originator. Our system provides (n-|attackers|)-anonymity for up to k-1 attackers and has little performance impact on dissemination. We show these results in a security analysis and performance evaluation based on a proof-of-concept prototype. Throughput rates between 10 and 100 kB/s are enough for many real applications with high privacy requirements, e.g., financial blockchain system., 16 pages, 5 figures

Opacity is a property of a system that captures whether certain event sequences (or certain states) are indistinguishable from other event sequences (or states) in the system. Opacity is used in analyzing privacy, secrecy, and other aspects of systems modeled by discrete-event systems. In this paper, we introduce the concept of minimal information release policies for non-opacity and the concept of mixed opacity. Mixed opacity policies are introduced as a holistic approach for solving problems that involve a combination of releasing information to make some objectives of the system opaque while making some other objectives non-opaque. We present a set of algorithms for information release under a mixed opacity policy. These algorithms compute policies in a system such that two given sublanguages are opaque, and at the same time, two other sublanguages in the same system are non-opaque. The application of mixed opacity is demonstrated on the Dining Cryptographers Problem. Note to Practitioners —Many organizations and companies must deal with maintaining privacy and secrecy and the protection of their intellectual property while at the same time revealing information to their employees so that they can properly do their jobs. In addition, to maintain transparency, companies and organizations must also reveal information to the public. In this paper, discrete-event system’s modeling is used to produce policies that capture the balance between privacy and transparency.

Most of the software model checkers available for code level verification can only verify safety properties since desired properties are specified by assertions. However, other temporal properties such as liveness cannot be verified with these tools. To tackle this problem, we develop a verification tool called UMC4M to verify full regular temporal properties of programs. UMC4M takes a modeling, simulation and verification language (MSVL) program M and a desired property specified by a propositional projection temporal logic (PPTL) formula P as its input. \(\lnot P\) is then translated to an MSVL program M. Thus, the property can be verified by checking whether there is an acceptable execution of “\(M~and~M'\)”, which can be solved with MSVL compiler MC. Further, UMC4M is used to verify the dining cryptographers protocol.

Hiding contents of users' messages has been successfully addressed before, while anonymization of message senders remains a challenge since users do not usually trust ISPs and messaging application providers. To resolve this challenge, several solutions have been proposed so far. Among them, the Dining Cryptographers network protocol (DC-net) provides the strongest anonymity guarantees. However, DC-net suffers from two critical issues that makes it impractical, i.e., (1) collision possibility and (2) vulnerability against disruptions. Apart from that, we noticed a third critical issue during our investigation. (3) DC-net users can be deanonymized after they publish at least three messages. We name this problem the short stability issue and prove that anonymity is provided only for a few cycles of message publishing. As far as we know, this problem has not been identified in the previous research works. In this paper, we propose Harmonized and Stable DC-net (HSDC-net), a self-organizing protocol for anonymous communications. In our protocol design, we first resolve the short stability issue and obtain SDC-net, a stable extension of DC-net. Then, we integrate the Slot Reservation and Disruption Management sub-protocols into SDC-net to overcome the collision and security issues, respectively. The obtained HSDC-net protocol can also be integrated into blockchain-based cryptocurrencies (e.g. Bitcoin) to mix multiple transactions (belonging to different users) into a single transaction in such a way that the source of each payment is unknown. This preserves privacy of blockchain users. Our prototype implementation shows that HSDC-net achieves low latencies that makes it a practical protocol.

This paper presents a framework for calculating measures of data integrity for programs in a small imperative language. The authors develop a Markov chain semantics for their language which calculates Clarkson and Schneider's definitions of data contamination, data suppression, program suppression and program transmission. The authors then propose their own definition of program integrity for probabilistic specifications. These definitions are based on conditional mutual information and entropy; they present a result relating them to mutual information, which can be calculated by a number of existing tools. The authors extend a quantitative information flow tool (CH-IMP) to calculate these measures of integrity and demonstrate this tool with examples including error correcting codes, the Dining Cryptographers protocol and the attempts by a number of banks to influence the Libor rate.

We introduce a framework for the symbolic verification of epistemic properties of programs expressed in a class of general-purpose programming languages. To this end, we reduce the verification problem to that of satisfiability of first-order formulae in appropriate theories. We prove the correctness of our reduction and we validate our proposal by applying it to two examples: the dining cryptographers problem and the ThreeBallot voting protocol. We put forward an implementation using existing solvers, and report experimental results showing that the approach can perform better than state-of-the-art symbolic model checkers for temporal-epistemic logic.

The increasing adoption of the Internet of Things introduces new threats that affect the privacy of users. Current privacy enhancing technologies are not sufficient to address all these new threats. This paper explains one of the most powerful protocols, namely DC-net. The DC-net protocol, while more than 30 years old, was never used in real-life due to its overhead and sensitivity with regards to disrupters. However, many improvements have been contributed to the original protocol, which is summarised in this paper. The main contribution of this work is the implementation of a proof-of-concept DC-net suited for constrained microcontroller-based devices. The challenges faced and the optimisations done throughout the implementation are presented.

A crucial goal in computer security is to protect sensitive information from unwanted disclosure. However, some leakage is often unavoidable, be it by design of the system or by technological limitations. The field of Quantitative Information Flow (QIF) is concerned with the quantification, and limitation, of information leakage in systems.

Users often wish to communicate anonymously on the Internet, for example, in group discussion or instant messaging forums. Existing solutions are vulnerable to misbehaving users, however, who may abuse their anonymity to disrupt communication. Dining Cryptographers Networks (DC-nets) leave groups vulnerable to denial-of-service and Sybil attacks; mix networks are difficult to protect against traffic analysis; and accountable voting schemes are unsuited to general anonymous messaging. dissent is the first general protocol offering provable anonymity and accountability for moderate-size groups, while efficiently handling unbalanced communication demands among users. We present an improved and hardened dissent protocol, define its precise security properties, and offer rigorous proofs of these properties. The improved protocol systematically addresses the delicate balance between provably hiding the identities of well-behaved users, while provably revealing the identities of disruptive users, a challenging task because many forms of misbehavior are inherently undetectable. The new protocol also addresses several nontrivial attacks on the original dissent protocol stemming from subtle design flaws.

In many applications, such as e-voting, it is imperative that the privacy reaches a level of unconditional security. In this context, protocols that verify that condition reach maximum interest. Probably, the most interesting of them is Non Interactive Dining cryptographers (NIDC), which relaxes the condition of concurrency online for all participants. NIDC proposes to store the vote on a table of slots, demanding that the selection of the location of each vote is truly random. However, the probability that two votes are accommodated in the same slot (collision) is positive. And if that event occurs, both votes are lost. This paper, after reviewing records which demonstrate that it is preferable to use multiple parallel channels while maintaining the original number of slots, proposes a systematic method to get the optimum for each of the parameters involved values: number of channels, measure them and probability level required for the event "no vote is lost." Additionally, the proposed solutions are enhanced, suggesting a way to work on collisions.

Sealed bid auctions are a popular means of high-stakes bidding, as they eliminate the temporal element from the auction process, allowing participants to take less emotional, more thoughtful decisions. In this paper, we propose a digital communication protocol for conducting sealed bid auctions with high stakes, where the anonymity of bids as well as other aspects of fairness must be protected. The Dining Cryptographers’ Protocol (denoted by DC) was presented by David Chaum in 1988. The protocol allows the participants to broadcast a message anonymously. In a recent paper (Another Twist in the Dining Cryptographers’ Protocol, submitted to the Journal of Cryptology) the authors propose a variant of the original DC eliminating its main disadvantages. In this paper we present a cryptographic protocol realizing anonymous sealed bid auctions, such as first price or Vickrey auction, based on this variant. The proposed scheme allows to identify at least one dishonest participant violating the protocol without using of Trusted Third Parties. Additionally, we require that bids are binding. It is achieved by enabling all participants acting in concert (the so-called “angry mob”) to find out the identity of the winner, in case the winner fails to make the purchase.

While many scenarios of anonymous communication can be solved by various famous classical techniques including mix nets or dining cryptographers (DC), an abundant amount of anonymous tasks remains open. In this paper, we present a solution to one such task. Our protocol serves as a private communication channel for quantum messages while ensuring that both the sender and the receiver stay anonymous in a set of all parties. Our protocol is a continuation of our previous work on anonymous transmission of quantum information. The protocol does not require trusted parties, and is secure against an active adversary. It can also withstand denial of service attacks. The protocol exhibits an advantage of quantum resources over classical because no classical solution is known (in the same security settings). Entanglement swapping technique is used to create "symmetry" in the protocol, which makes it very transparent and easier to analyze. The security analysis we present is heavily based on our previous work on quantum anonymous communication. The task we implement is also a nice illustration of a cryptographic task where two parties in a multi-party protocol can be dishonest at the same time, but are not cooperating.

The past two decades have seen a growing interest in methods for anonymous communication on the Internet, both from the academic community and the general public. Several system designs have been proposed in the literature, of which a number have been implemented and are used by diverse groups, such as journalists, human rights workers, the military, and ordinary citizens, to protect their identities on the Internet. In this work, we survey the previous research done to design, develop, and deploy systems for enabling private and anonymous communication on the Internet. We identify and describe the major concepts and technologies in the field, including mixes and mix networks, onion routing, and Dining Cryptographers networks. We will also review powerful traffic analysis attacks that have motivated improvements and variations on many of these anonymity protocols made since their introduction. Finally, we will summarize some of the major open problems in anonymous communication research and discuss possible directions for future work in the field.

Stepwise refinement is a crucial conceptual tool for system development, encouraging program construction via a number of separate correctness-preserving stages which ideally can be understood in isolation. A crucial conceptual component of security is an adversary's ignorance of concealed information. We suggest a novel method of combining these two ideas. Our suggestion is based on a mathematical definition of ''ignorance-preserving'' refinement that extends classical refinement by limiting an adversary's access to concealed information: moving from specification to implementation should never increase that access. The novelty is the way we achieve this in the context of sequential programs. Specifically we give an operational model (and detailed justification for it), a basic sequential programming language and its operational semantics in that model, a ''logic of ignorance'' interpreted over the same model, then a program-logical semantics bringing those together - and finally we use the logic to establish, via refinement, the correctness of a real (though small) protocol: Rivest's Oblivious Transfer. A previous report^@? treated Chaum's Dining Cryptographers similarly. In passing we solve the Refinement Paradox for sequential programs.

International audience; We consider a framework in which anonymity protocols are interpreted as noisy channels in the information-theoretic sense, and we explore the idea of using the notion of capacity as a measure of the loss of anonymity. Such idea was already suggested by Moskowitz, Newman and Syverson, in their analysis of the covert channel that can be created as a result of non-perfect anonymity. We consider the case in which some leak of information is intended by design, and we introduce the notion of conditional capacity to rule out this factor, thus retrieving a natural correspondence with the notion of anonymity. Furthermore, we show how to compute the capacity and the conditional capacity when the anonymity protocol satisfies certain symmetries. We also investigate how the adversary can test the system to try to infer the user's identity, and we study how his probability of success depends on the characteristics of the channel. We then illustrate how various notions of anonymity can be expressed in this framework, and show the relation with some definitions of probabilistic anonymity in literature. Finally, we show how to compute the matrix of the channel (and hence the capacity and conditional capacity) using model checking.

When modelling cryto-protocols by means of process calculi which express both nondeterministic and probabilistic behavior, it is customary to view the scheduler as an intruder. It has been established that the traditional scheduler needs to be carefully calibrated in order to more accurately reflect the intruder's capabilities for controlling communication channels. We propose such a class of schedulers through a semantic variant called PPCνσ, of the Probabilistic Poly-time Calculus (PPC) of Mitchell et al. [J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science, 353:118–164, 2006] and we illustrate the pertinence of our approach by an extensive study of the Dining Cryptographers (DCP) [David Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. J. Cryptology, 1(1):65–75, 1988] protocol. Along these lines, we define a new characterization of Mitchell et al.'s observational equivalence [J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science, 353:118–164, 2006] more suited for taking into account any observable trace instead of just a single action as required in the analysis of the DCP.

International audience; Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described probabilistically. In this paper we propose a notion of weak probabilistic anonymity, where weak refers to the fact that some amount of probabilistic information may be revealed by the protocol. This information can be used by an observer to infer the likeliness that the action has been performed by a certain user. The aim of this work is to study the degree of anonymity that the protocol can still ensure, despite the leakage of information. We illustrate our ideas by using the example of the dining cryptographers with biased coins. We consider both the cases of nondeterministic and probabilistic users. Correspondingly, we propose two notions of weak anonymity and we investigate their respective dependencies on the biased factor of the coins.

In many applications, such as e-voting, it is imperative that the privacy scope unconditional security levels, i.e. that it is protected regardless of the resources and the time available to attack. In this context, protocols that verify that condition reach maximum interest. Probably, the most interesting of them is Non Interactive Dining cryptographers (NIDC), that relaxes the condition of concurrency online for all participants. This paper proposes a new technique, based in parallel channels, to optimize the storage of the votes in the model NIDC.

This paper presents a framework for calculating measures of data integrity for programs in a small imperative language. We develop a Markov chain semantics for our language which calculates Clarkson and Schneider’s definitions of data contamination and suppression. These definitions are based on conditional mutual information and entropy; we present a result relating them to mutual information, which can be calculated by a number of existing tools. We extend a quantitative information flow tool (CH-IMP) to calculate these measures of integrity and demonstrate this tool with examples based on error correcting codes, the Dining Cryptographers protocol and the attempts by a number of banks to influence the Libor rate.

We present a compiler that translates a multi-agent systems specification given in the formalism of Interpreted Systems into an SMV program. We show how an SMV model checker can be coupled with a Kripke model editor (Akka) to allow for the mechanical verification of epistemic properties of multi-agent systems. We apply this methodology to the verification of a communication protocol — the dining cryptographers.

In this paper we focus on sender-anonymous channels (a.k.a. Dining Cryptographers networks) and present a construction requiring a very low (constant) number of rounds of interaction while tolerating actively malicious behavior by some of the participants (up to less than half of them). Our construction is unconditionally secure (meaning that no bounds are placed on the computational power of the adversary), makes black-box use of a verifiable secret sharing (VSS) protocol, and is based on a special-purpose secure multiparty computation protocol implementing the method of "throwing darts;" its round complexity is essentially equal to that of the VSS protocol.In addition, since broadcast cannot be simulated in a point-to-point network when a third or more of the participants are corrupt, it is impossible to construct VSS (and, more generally, any other basic multiparty protocol) in this setting without using a "physical broadcast channel," and a recent line of research has sought to minimize the use of this expensive resource. Our anonymous channel protocol's reduction to VSS is broadcast-round-preserving, thus making the fewest (known to date) calls to the broadcast channel while running in an overall constant number of rounds.Finally, anonymous channels play an important role in the setup phase of an authentication technique known as pseudosignatures, which then may be used to simulate authenticated Byzantine agreement protocols in the information-theoretic setting. Plugging in our anonymous channel translates into a fast (and broadcast-efficient) pseudosignature construction.

We describe an algorithm for fully-anonymous broadcast in large-scale networks. The protocol is similar to the dining cryptographers networks (DC-Nets) in that both are based on secure multi-party computation (MPC) techniques. However, we address the weaknesses of DC-Nets, which are poor scalability and vulnerability to jamming attacks. When compared to the state-of-the-art, our protocol reduces the total bit complexity from O(n2) to O(n) per anonymous message sent in a network of size n at the expense of an increase in total latency from O(1) to polylog(n). Our protocol can tolerate up to 1/3 dishonest parties, which are controlled by a static computationally-unbounded Byzantine adversary.

The Dining Cryptographer network (or DC-net) is a privacy preserving communication protocol devised by David Chaum for anonymous message publication. A very attractive feature of DC-nets is the strength of its security, which is inherent in the protocol and is not dependent on other schemes, like encryption. Unfortunately the DC-net protocol has a level of complexity that causes it to suffer from exceptional communication overhead and implementation difficulty that precludes its use in many real-world use-cases. We have designed and created a DC-net implementation that uses a pure client- server model, which successfully avoids much of the complexity inherent in the DC-net protocol. We describe the theory of DC- nets and our pure client-server implementation, as well as the compromises that were made to reduce the protocol's level of complexity. Discussion centers around the details of our implementation of DC-net. Keywords—Dining Cryptographer network; Privacy; sender- untraceability I. INTRODUCTION The issue of privacy and anonymity on the Internet has become a challenging one, especially with the growing influence that the Internet has on our day-to-day social lives. With the increased use of social networking sites and mobile Internet based communication, being anonymous and maintaining privacy has becoming something that the average computer has great difficulty in achieving. Preserving the anonymity of the communicating parties is crucial in situations where knowledge of the identity of the source of communicated messages could create a conflict of interest, jeopardize the integrity of a process or endanger the participants. The concept of maintaining anonymity is simple to conceive. However, they can be rather difficult to implement. The trails left by the protocols and technologies involved in digital communication can be difficult to erase or hide to a point where the identity of the communicating parties is not exposed. The trails created in these communications are often required for the communication itself often to maintain a quality of service or integrity of the message being communicated. This paper describes a digital, computer based form of communication that preserves the anonymity of all communicating parties. The program takes heavy influence from David Chaum's Dining Cryptographers problem and the DC Net concept. A. Background

A novel electronic voting scheme is proposed which is quite suitable for small scale election settings. An outstanding characteristic of the design is its guarantee of unconditionally perfect ballot secrecy. It satisfies self-tallying, fairness and verifiability. Disruption of the result of an election equals to breaking the Discrete Logarithm Problem. Our scheme is built on top of the DC-net(dining cryptographers network) anonymous broadcast protocol. It needs no trusted authority to guarantee its security, but assumes a complete network of secure private channels between voters.

Anonymous communication protocols must achieve two seemingly contradictory goals: privacy (informally, they must guarantee the anonymity of the parties that send/receive information), and robustness (informally, they must ensure that the messages are not tampered). However, the long line of research that defines and analyzes the security of such mechanisms focuses almost exclusively on the former property and ignores the latter. In this paper, we initiate a rigorous study of robustness properties for anonymity protocols. We identify and formally define, using the style of modern cryptography, two related but distinct flavors of robustness. Our definitions are general (e.g. they strictly generalize the few existent notions for particular protocols) and flexible (e.g. they can be easily adapted to purely combinatorial/probabilistic mechanisms). We demonstrate the use of our definitions through the analysis of several anonymity mechanisms (Crowds, broadcast-based mix-nets, DC-nets, Tor). Notably, we analyze the robustness of a protocol by Golle and Juels for the dining cryptographers problem, identify a robustness-related weakness of the protocol, and propose and analyze a stronger version.

Chaum’s Dining Cryptographers protocol crystallises the essentials of security just as other famous diners once demonstrated deadlock and livelock: it is a benchmark for security models and their associated verification methods. Here we give a correctness proof of the Cryptographers in a new style, one in which stepwise refinement plays a prominent role. Furthermore, our proof applies to arbitrarily many diners: that is unusually general. The proof is based on the Shadow Security Model, which integrates non-interference and program refinement: with it, we try to make a case that stepwise development of security protocols is not only possible but also actually to be recommended. It benefits from more than 3 decades of experience of how layers of abstraction can both simplify the design process and make its outcomes more likely to be correct.

Publisher Summary This chapter provides an introduction to dining cryptographers (DC), which allows people to broadcast messages to a group without revealing identities. DC networks offer a good opportunity to provide unconditional security against traffic analysis. No one can detect the broadcaster if the nodes of the network keep their coin flips private. Nor can anyone determine the recipient if the messages are encrypted. DC nets offer an ideal way to obscure the source of a transmission. If this transmission is encrypted, then only the intended recipient is able to read it. The system is secure if all of the information about the coin flips is kept secret. Otherwise, the group can track down the sender by revealing all of this information. The solution is easy to describe because many of the difficulties of implementing it on a computer network are left out of the picture. The major limitation to DC nets is the high cost of information traffic. Every member of the network must flip coins with their neighbor and then broadcast this information to the group. This can be done in blocks, but it is still a significant cost.

The dining cryptographers network (or DC-net) is a seminal technique devised by Chaum to solve the dining cryptographers problem — namely, how to send a boolean-OR bit anonymously from a group of participants. In this paper, we investigate the weaknesses of DC-nets, study alternative methods and propose a new way to tackle this problem. Our protocol, Anonymous Veto Network (or AV-net), overcomes all the major limitations of DC-nets, including the complex key setup, message collisions and susceptibility to disruptions. While DC-nets are unconditionally secure, AV-nets are computationally secure under the Decision Diffie-Hellman (DDH) assumption. An AV-net is more efficient than other techniques based on the same public-key primitives. It requires only two rounds of broadcast and the least computational load and bandwidth usage per participant. Furthermore, it provides the strongest protection against collusion — only full collusion can breach the anonymity of message senders.

The Dining Cryptographers problem studies how to securely compute the boolean-OR function while preserving the privacy of each input bit. Since its first introduction by Chaum in 1988, it has attracted a number of solutions over the past twenty years. In this paper, we propose an exceptionally efficient solution: Anonymous Veto Network (or AV-net). Our protocol is provably secure under the Decision Diffie-Hellman (DDH) and random oracle assumptions, and is better than past work in the following ways. It provides the strongest protection of each input's privacy against collusion attacks; it requires only two rounds of broadcast, fewer than any other solution; the computational load and bandwidth usage are the least among the available techniques; and the efficiency of our protocol is achieved without relying on any private channels or trusted third parties. Overall, the efficiency of our protocol seems as good as one may hope for.

Security and probability are both artefacts that we hope to bring increasingly within the reach of refinement-based Formal Methods; although we have worked on them separately, in the past, the goal has always been to bring them together. In this report we describe our ongoing work in that direction: we relate it to a well known problem in security, Chaum's Dining Cryptographers , where the various criteria of correctness that might apply to it expose precisely the issues we have found to be significant in our efforts to deal with security, probability and abstraction all at once. Taking our conviction into this unfamiliar and demanding territory, that abstraction and refinement are the key tools of software development, has turned out to be an exciting challenge.

We introduce the first protocol for the anonymous transmission of a quantum state that is information-theoretically secure against an active adversary, without any assumption on the number of corrupt participants. The anonymity of the sender and receiver is perfectly preserved, and the privacy of the quantum state is protected except with exponentially small probability. Even though a single corrupt participant can cause the protocol to abort, the quantum state can only be destroyed with exponentially small probability: if the protocol succeeds, the state is transferred to the receiver and otherwise it remains in the hands of the sender (provided the receiver is honest).

The dining cryptographers network (or DC-net) is a seminal technique devised by Chaum to solve the dining cryptographers problem -- namely, how to send a boolean-OR bit anonymously from a group of participants. In this paper, we investigate the weaknesses of DC-nets, study alternative methods and propose a new way to tackle this problem. Our protocol, Anonymous Veto Network (or AV-net), overcomes all the major limitations of DC-nets, including the complex key setup, message collisions and susceptibility to disruptions. While DC-nets are unconditionally secure, AV-nets are computationally secure under the Decision Diffie-Hellman (DDH) assumption. An AV-net is more efficient than other techniques based on the same public-key primitives. It requires only two rounds of broadcast and the least computational load and bandwidth usage per participant. Furthermore, it provides the strongest protection against collusion -- only full collusion can breach the anonymity of message senders.

In a Dining Cryptographers network, the anonymity level raises with the number of participating users. This paper studies strategic behavior based on game theory. Strategic user behavior can cause sudden changes to the number of system participants and, in consequence, degrade anonymity. This is caused by system parameters that influence strategic behavior. Additionally, conflicting goals of participants result in dilemma games. Properties of message coding, e.g. collision robustness and disrupter identification, change the game outcome by preventing dilemmas and, therefore, enhance anonymity. Properties of anonymity metrics are proposed that allow for strategic user behavior.

This paper provides a framework for specification and verification of intelligent agent-based systems, with the emphasis on their cognitive and reactive features. We use an epistemic transition system to specify the agents and an epistemic synchronous product to specify the multi-agent system. We verify the system by means of a special action-based logic - ACTLW for Epistemic Reasoning (ACTLW stands for Action Computation Tree Logic with Unless Operator). Using temporal and epistemic operators we create the appropriate formulae to check whether the relevant property holds, or the protocol works within the given conditions. We test our method by the example of security communication protocol called Dining Cryptographers.

We introduce a simple procedural probabilistic programming language which is suitable for coding a wide variety of randomised algorithms and protocols. This language is interpreted over finite datatypes and has a decidable equivalence problem. We have implemented an automated equivalence checker, which we call apex, for this language, based on game semantics. We illustrate our approach with three non-trivial case studies: (i) Herman's self-stabilisation algorithm; (ii) an analysis of the average shape of binary search trees obtained by certain sequences of random insertions and deletions; and (iii) the problem of anonymity in the Dining Cryptographers protocol. In particular, we record an exponential speed-up in the latter over state-of-the-art competing approaches. © 2008 Springer-Verlag Berlin Heidelberg.

Anonymity is the property of maintaining secret the identity of users performing a certain action. Anonymity protocols often use random mechanisms which can be described probabilistically. In this paper, we propose a probabilistic process calculus to describe protocols for ensuring anonymity, and we use the notion of relative entropy from information theory to measure the degree of anonymity these protocols can guarantee. Furthermore, we prove that the operators in the probabilistic process calculus are non-expansive, with respect to this measuring method. We illustrate our approach by using the example of the Dining Cryptographers Problem.

Dining cryptographers networks (or DC-nets) are a privacy-preserving primitive devised by Chaum for anonymous message publication. A very attractive feature of the basic DC-net is its non-interactivity. Subsequent to key establishment, players may publish their messages in a single broadcast round, with no player-to-player communication. This feature is not possible in other privacy-preserving tools like mixnets. A drawback to DC-nets, however, is that malicious players can easily jam them, i.e., corrupt or block the transmission of messages from honest parties, and may do so without being traced.

Security protocols are designed to meet particular security properties. In order to analyse such protocols formally, it is necessary to provide a formal definition of the property that they are intended to provide. This paper is concerned with the property of anonymity. It proposes a definition of anonymity within the CSP notation, discusses the approach taken by CSP to anonymity with respect to different viewpoints, and illustrates this approach on some toy examples, and then applies it to a machine-assisted analysis of the dining cryptographers example and some variants.

A technique based on public key cryptography is presented that allows an electronic mail system to hide who a participant communicates with as well as the content of the communication - in spite of an unsecured underlying telecommunication system. The technique does not require a universally trusted authority. One correspondent can remain anonymous to a second, while allowing the second to respond via an untraceable return address. The technique can also be used to form rosters of untraceable digital pseudonyms from selected applications. Applicants retain the exclusive ability to form digital signatures corresponding to their pseudonyms. Elections in which any interested party can verify that the ballots have been properly counted are possible if anonymously mailed ballots are signed with pseudonyms from a roster of registered voters. Another use allows an individual to correspond with a record-keeping organization under a unique pseudonym, which appears in a roster of acceptable clients.

Privacy requires more than just encryption of data before and during transmission. Privacy would actually demand hiding the sheer fact that communication takes place. This requires to protect meta-data from observation. We motivate the need for strong privacy protection in a smart home use case by highlighting the privacy issues that cannot be solved by confidentiality mechanisms like encryption alone. Our solution is a implementation of DC-net on Re-Mote sensor nodes running Contiki OS. From this, we conclude that the computational and network overheads imposed by these techniques do not make them impractical to use in the IoT. To the best knowledge of the authors, this is the first implementation of DC-net on sensors. Alongside, we provide a survey of the required strong cryptographic security mechanisms, like encryption of communication, to be in place. We describe how the current existing techniques can be facilitated to achieve unobservable communication for the IoT. This includes mechanisms for encrypted IoT communication like DTLS or message authentication like ECDSA signatures on IoT devices. For readers unfamiliar with the concepts of MIXing and DC-net, we explain and analyse how those techniques, formerly used to provide private communication in the Internet, can be applied to the IoT. We briefly survey what complementary features from the IoT architecture are helpful in providing strong protection in this particular use case. Finally, we state some recommendations hoping that following these will enable us to reduce the privacy invasiveness of the IoT on all levels. We think that this will be indispensable if IoT devices shall become a part of our daily lives without rendering us into an Orwellian society.

Keeping confidential who sends which messages, in a world where any physical transmission can be traced to its origin, seems impossible. The solution presented here is unconditionally or cryptographically secure, depending on whether it is based on one-time-use keys or on public keys, respectively. It can be adapted to address efficiently a wide variety of practical considerations.