Name
Abstract | ||
|---|---|---|
In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated analysis of equivalence properties is limited compared to trace properties, e.g., modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure for verifying equivalences on finite processes, i.e., without replication, for protocols that rely on various cryptographic primitives including exclusive or (xor). We have implemented our procedure in the tool AKISS, and successfully used it on several case studies that are outside the scope of existing tools, e.g., unlinkability on various RFID protocols, and resistance against guessing attacks on protocols that use xor. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/CSF.2017.22 | 2017 IEEE 30th Computer Security Foundations Symposium (CSF) |
Keywords | Field | DocType |
tool support,automated analysis,equivalence properties,finite processes,RFID protocols,symbolic verification,privacy-type properties,security protocols,process equivalences,modeling authentication,cryptographic primitives,AKISS tool | Authentication,Cryptographic protocol,Exclusive or,Computer science,Cryptography,Computer security,Secrecy,Cryptographic primitive,Theoretical computer science,Equivalence (measure theory),Anonymity | Conference |
ISSN | ISBN | Citations |
1063-6900 | 978-1-5386-3218-5 | 2 |
PageRank | References | Authors |
0.36 | 31 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| David Baelde | 1 | 155 | 13.37 |
| Stéphanie Delaune | 2 | 866 | 41.94 |
| Ivan Gazeau | 3 | 18 | 2.08 |
| Steve Kremer | 4 | 46 | 5.30 |