User-Guided Verification of Security Protocols via Sound Animation
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911123446431744 |
|---|---|
| author | Ye, Kangfeng Metere, Roberto Yadav, Poonam |
| author_facet | Ye, Kangfeng Metere, Roberto Yadav, Poonam |
| contents | Current formal verification of security protocols relies on specialized researchers and complex tools, inaccessible to protocol designers who informally evaluate their work with emulators. This paper addresses this gap by embedding symbolic analysis into the design process. Our approach implements the Dolev-Yao attack model using a variant of CSP based on Interaction Trees (ITrees) to compile protocols into animators -- executable programs that designers can use for debugging and inspection. To guarantee the soundness of our compilation, we mechanised our approach in the theorem prover Isabelle/HOL. As traditionally done with symbolic tools, we refer to the Diffie-Hellman key exchange and the Needham-Schroeder public-key protocol (and Lowe's patched variant). We demonstrate how our animator can easily reveal the mechanics of attacks and verify corrections. This work facilitates security integration at the design level and supports further security property analysis and software-engineered integrations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_00676 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | User-Guided Verification of Security Protocols via Sound Animation Ye, Kangfeng Metere, Roberto Yadav, Poonam Cryptography and Security Logic in Computer Science Current formal verification of security protocols relies on specialized researchers and complex tools, inaccessible to protocol designers who informally evaluate their work with emulators. This paper addresses this gap by embedding symbolic analysis into the design process. Our approach implements the Dolev-Yao attack model using a variant of CSP based on Interaction Trees (ITrees) to compile protocols into animators -- executable programs that designers can use for debugging and inspection. To guarantee the soundness of our compilation, we mechanised our approach in the theorem prover Isabelle/HOL. As traditionally done with symbolic tools, we refer to the Diffie-Hellman key exchange and the Needham-Schroeder public-key protocol (and Lowe's patched variant). We demonstrate how our animator can easily reveal the mechanics of attacks and verify corrections. This work facilitates security integration at the design level and supports further security property analysis and software-engineered integrations. |
| title | User-Guided Verification of Security Protocols via Sound Animation |
| topic | Cryptography and Security Logic in Computer Science |
| url | https://arxiv.org/abs/2410.00676 |