Rule-based Programs describing Internet Security Protocols

RWTH Aachen Technical Report AIB-2004-04. Colloque avec actes et comité de lecture. Internationale.International audienceWe present a low-level specification language used for describing real Internet security protocols. Specifications are automatically generated by a compiler, from TLA-based high-level descriptions of the protocols. The results are rule-based programs containing all the information needed for either implementing the protocols, or verifying some security properties. This approach has already been applied to several well-known Internet security protocols, and the generated programs have been successfully used for finding some attacks