Proverif specification generation fails when using Timer type in messages
So types in functions are not checked for before proverif generation (e.g., syntax checking)
So types in functions are not checked for before proverif generation (e.g., syntax checking)