Sciweavers

Share
CSFW
1998
IEEE

Proving Security Protocols with Model Checkers by Data Independence Techniques

9 years 7 months ago
Proving Security Protocols with Model Checkers by Data Independence Techniques
Model checkers such as FDR have been extremely e ective in checking for, and nding, attacks on cryptographic protocols { see, for example 11, 12, 14] and many of the papers in 3]. Their use in proving protocols has, on the other hand, generally been limited to showing that a given small instance, usually restricted by the niteness of some set of resources such as keys and nonces, is free of attacks. While for speci c protocols there are frequently good reasons for supposing that this will nd 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 elds can be used to achieve the illusion that nodes can call upon an in nite supply of di erent nonces, keys, etc., even though the actual types used for these things remain nite. 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, within certain limits, a nite-state ru...
A. W. Roscoe
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1998
Where CSFW
Authors A. W. Roscoe
Comments (0)
books