Loading...
Please wait, while we are loading the content...
Similar Documents
Electronic Communications of the EASST Volume 66 ( 2013 ) Proceedings of the Automated Verification of Critical Systems ( AVoCS 2013 ) Verifying a Mix Net in CSP
| Content Provider | Semantic Scholar |
|---|---|
| Author | Stathakidis, Efstathios Williams, David Moreton Heather, James |
| Copyright Year | 2014 |
| Abstract | A Mix Net is a cryptographic protocol that tries to unlink the correspondence between its inputs and its outputs. In this paper, we formally analyse a Mix Net using the process algebra CSP and its associated model checker FDR. The protocol that we verify removes the reliance on a Web Bulletin Board during the mixing process: rather than communicating via a Web Bulletin Board, the protocol allows the mix servers to communicate directly, exchanging signed messages and maintaining their own records of the messages they have received. Mix Net analyses in the literature are invariably focused on safety properties; important liveness properties, such as deadlock freedom, are wholly neglected. This is an unhappy omission, however, since a Mix Net that produces no results is of little use. Here we verify that the Mix Net is guaranteed to terminate, outputting a provably valid mix agreed upon by a majority of mix servers, under the assumption that a majority of them act according to the protocol. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://journal.ub.tu-berlin.de/eceasst/article/download/896/883 |
| Alternate Webpage(s) | https://journal.ub.tu-berlin.de/eceasst/article/download/896/883/ |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
