|
Abstract : |
A logical environment for specifying and proving authentication protocols correct is presented. Protocols are modeled as parametric, innite-state systems, and speci ed using a multiset rewriting formalism, with universal quantication providing a way to choose new values like nonces. We show that secrecy and condentiality properties can be veried using a technique based on symbolic model-checking and uni cation. Unlike previous approaches based on model-checking, we make use of a backward, bottom-up evaluation strategy which does not pose any restriction on the number of principals or the number of simultaneous sessions involved. We report on some preliminary experiments on the paradigmatic Needham-Schroeder public-key authentication protocol., |
