Model checking cryptographic protocols subject to combinatorial attack.
We introduce an approach to model checking cryptographic protocols that use hashing too weak to resist combinatorial attacks. Typically such hashing is used when an extremely low bandwidth channel, such as a human user, is employed to transmit its output. This leads to two opportunities for attack:...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Published: |
2011
|
| _version_ | 1826272481406615552 |
|---|---|
| author | Roscoe, T Nguyen., L |
| author_facet | Roscoe, T Nguyen., L |
| author_sort | Roscoe, T |
| collection | OXFORD |
| description | We introduce an approach to model checking cryptographic protocols that use hashing too weak to resist combinatorial attacks. Typically such hashing is used when an extremely low bandwidth channel, such as a human user, is employed to transmit its output. This leads to two opportunities for attack: deducing a weak value from its properties and discovering alternative ways to produce a given weak value. The first of these proves a natural extension to established protocol modelling approaches, but for the second we require something more novel. We propose an approach based on taking snapshots of the intruder memory. |
| first_indexed | 2024-03-06T22:13:14Z |
| format | Journal article |
| id | oxford-uuid:52875969-f7ae-4575-a2be-558dbe46277a |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:13:14Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:52875969-f7ae-4575-a2be-558dbe46277a2022-03-26T16:26:03ZModel checking cryptographic protocols subject to combinatorial attack.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:52875969-f7ae-4575-a2be-558dbe46277aDepartment of Computer Science2011Roscoe, TNguyen., LWe introduce an approach to model checking cryptographic protocols that use hashing too weak to resist combinatorial attacks. Typically such hashing is used when an extremely low bandwidth channel, such as a human user, is employed to transmit its output. This leads to two opportunities for attack: deducing a weak value from its properties and discovering alternative ways to produce a given weak value. The first of these proves a natural extension to established protocol modelling approaches, but for the second we require something more novel. We propose an approach based on taking snapshots of the intruder memory. |
| spellingShingle | Roscoe, T Nguyen., L Model checking cryptographic protocols subject to combinatorial attack. |
| title | Model checking cryptographic protocols subject to combinatorial attack. |
| title_full | Model checking cryptographic protocols subject to combinatorial attack. |
| title_fullStr | Model checking cryptographic protocols subject to combinatorial attack. |
| title_full_unstemmed | Model checking cryptographic protocols subject to combinatorial attack. |
| title_short | Model checking cryptographic protocols subject to combinatorial attack. |
| title_sort | model checking cryptographic protocols subject to combinatorial attack |
| work_keys_str_mv | AT roscoet modelcheckingcryptographicprotocolssubjecttocombinatorialattack AT nguyenl modelcheckingcryptographicprotocolssubjecttocombinatorialattack |