Soundness Conditions for Cryptographic Algorithms and Parameters Abstractions in Formal Security Protocol Models

When using formal methods, security protocols are usually modeled with a high level of abstraction. In particular, encryption is assumed to be perfect and cryptographic algorithms and their parameters are often abstracted away. This paper states a set of constraints under which, if an abstract protocol model is secure, then a refined model, which takes into account cryptographic algorithms and parameters, is implied to be secure too. The paper also indicates possible exploitations of this result.