Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866929584373497856 |
|---|---|
| author | Yatapanage, Nisansala P. Jones, Cliff B. |
| author_facet | Yatapanage, Nisansala P. Jones, Cliff B. |
| contents | The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are often hidden and are difficult to identify, making it unclear whether a given protocol is safe to deploy into a particular environment. Rely/guarantee provides a mechanism for abstractly reasoning about the interference from the environment. Using this approach, the assumptions are made clear and precise. This paper investigates this approach on the Needham-Schroeder Public Key protocol, showing that the technique can effectively uncover the assumptions under which the protocol can withstand attacks from intruders. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2311_15189 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols Yatapanage, Nisansala P. Jones, Cliff B. Logic in Computer Science Software Engineering The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are often hidden and are difficult to identify, making it unclear whether a given protocol is safe to deploy into a particular environment. Rely/guarantee provides a mechanism for abstractly reasoning about the interference from the environment. Using this approach, the assumptions are made clear and precise. This paper investigates this approach on the Needham-Schroeder Public Key protocol, showing that the technique can effectively uncover the assumptions under which the protocol can withstand attacks from intruders. |
| title | Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols |
| topic | Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2311.15189 |