Proving security protocols with model checkers by data independence techniques.
Saved in:
| Title: | Proving security protocols with model checkers by data independence techniques. |
|---|---|
| Authors: | Roscoe, A.W., Broadfoot, P.J. |
| Source: | Journal of Computer Security. 1999, Vol. 7 Issue 2/3, p147. 44p. 1 Diagram. |
| Subjects: | Computer network protocols, CSP (Computer program language) |
| Abstract: | Model checkers such as FDR have been extremely effective in checking for, and finding, attacks on cryptographic protocols -- see, for example, [16,20] and many of the papers in [7]. Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually restricted by the finiteness of some set of resources such as keys and nonces, is free of attacks. While for specific protocols there are frequently good reasons for supposing that this will find any attack, it leaves a substantial gap in the method. The purpose of this paper is to show how techniques borrowed from data independence and related fields can be used to achieve the illusion that nodes can call upon an infinite supply of different nonces, keys, etc., even though the actual types used for these things remain finite. It is thus possible to create models of protocols in which nodes do not have to stop after a small number of runs, and to claim that a finite-state run on a model checker has proved that a given protocol is free from attacks which could be constructed in the model used. We develop our methods via a series of case studies, discovering a number of methods for restricting the number of states generated in attempted proofs, and using two distinct approaches to protocol specification. [ABSTRACT FROM AUTHOR] |
| Copyright of Journal of Computer Security is the property of Sage Publications Inc. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
|
Full text is not displayed to guests.
Login for full access.
|
|
Be the first to leave a comment!
