Abstract: This paper researches the computational soundness of the ability description about a formal attacker in a formal analytical system when security protocols use only data integrity algorithms. Firstly, the authors assume that a computational attacker is more powerful than a formal attacker. Secondly, an attack experiment is constructed. And thirdly, a contradiction is proved about the output of the computational attack of the attack experiment against the security definitions of signature algorithms and keyed hash functions. So the conclusion is obtained that all the messages created by a computational attacker belong to the message closure which can be created by a formal attacker. Based on the conclusion, one can construct or improve a formal analytical system to make sound computations.

Key words: security protocols, formal attacker, computational attacker