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...

• Type: Conference
• Year: 1998
• Where: CSFW
• Authors: A. W. Roscoe
• Keywords: Cryptographic Protocols, CSFW 1998, Model Checker, Security Privacy, Small Instance