have led to a much too large REC specification); (iii) supplementary test vectors intended to specifically check for certain aspects (byte permutations and message segmentation) that were not enough covered by the above tests; this was done by introducing a function acting as a pseudo-random message generator (see Annex \[ANNEX-REC-MESSAGE\]).

-   Our model is [*confluent*]{}. This is easy to see, because all constructors are free and all the rules defining non-constructors have disjoint patterns and mutually exclusive premises; for safety, the disjunction of patterns and exclusion of guards has been checked mechanically by translating the REC specification to the Opal language [@Didrich-Fett-Gerke-et-al-94], whose compiler emits warnings in presence of “ambiguous” (i.e., nondeterministic) rules.

-   Our model is [*terminating*]{}. This has been verified by automatically translating our REC model into the input formalism TRS of the AProVE tool [@Giesl-Brockschmidt-Emmes-et-al-14], which produced a proof of quasi-decreasingness in 76 steps.

-   Our model was [*validated*]{}. We checked that the REC specification satisfies all the aforementioned test vectors. Because it enjoys the confluence and termination properties, all rewrite strategies should lead to the same result. Using a software framework[^2] under development at INRIA Grenoble, we automatically translated our REC model into thirteen different languages: 