|
| << previous | next >> |
Journal description
All volumes of the corresponding journal
All issues of the corresponding volume
All articles of the corresponding issues
Details for article 4 of 8 found articles
| Title: |
LTL model-checking for security protocols |
| Author: |
Carbone, Roberto |
| Appeared in: |
AI communications |
| Paging: | Volume 24 (2011) nr. 3 pages 281-283 |
| Year: |
2011-11-09 |
| Contents: |
This thesis is about the application of automated reasoning techniques to the formal analysis of security protocols. More in detail, it proposes a general model-checking framework for security protocols based on a set-rewriting formalism that, coupled with the use of Linear Temporal Logic, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analyzers. The approach successfully combines encoding techniques originally developed for planning with bounded model-checking techniques. The effectiveness of the approach proposed is assessed against the formal analysis of relevant security protocols, with the detection of a severe security flaw in Google's SAML-based SSO for Google Apps and a previously unknown attack on a patched version of the ASW contract-signing protocol. |
| Publisher: |
IOS Press |
| Source file: |
Elektronische Wetenschappelijke Tijdschriften |
Details for article 4 of 8 found articles
| << previous | next >> |