Formal Computational Unlinkability Proofs of RFID Protocols
| Title | Formal Computational Unlinkability Proofs of RFID Protocols |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Comon, H., Koutsos, A. |
| Conference Name | 2017 IEEE 30th Computer Security Foundations Symposium (CSF) |
| Date Published | Aug. 2017 |
| Publisher | IEEE |
| ISBN Number | 978-1-5386-3217-8 |
| Keywords | communication complexity, computational complete symbolic attacker, computational model, Computational modeling, cryptographic protocols, cryptography, formal computational unlinkability proofs, Hash functions, Human Behavior, human factors, Protocols, pubcrawl, radiofrequency identification, Resiliency, RFID, RFID protocols, RFIDs, security of data, security protocols, theorem proving, Tools, Turing machines, unlinkability |
| Abstract | We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: 1) to design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF). 2) to formalize computational unlinkability in the model. 3) to illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the omputational model. |
| URL | https://ieeexplore.ieee.org/document/8049714/ |
| DOI | 10.1109/CSF.2017.9 |
| Citation Key | comon_formal_2017 |
- pubcrawl
- unlinkability
- Turing machines
- tools
- Theorem Proving
- security protocols
- security of data
- RFIDs
- RFID protocols
- RFID
- Resiliency
- radiofrequency identification
- communication complexity
- Protocols
- Human Factors
- Human behavior
- Hash functions
- formal computational unlinkability proofs
- Cryptography
- Cryptographic Protocols
- Computational modeling
- computational model
- computational complete symbolic attacker