11. A computer-readable recording medium containing a reactive system safety verification computer program, said reactive system being an electronic system, which is a cipher communication system or control system for a nuclear reactor or aircraft, said computer program being executed by a computer comprising a processing unit and a recording unit, and said computer program comprising: a first program code which makes said processing unit to accept an input of a procedure represented by a set of function symbols, a set of rewriting rules, a set of axioms, a set of first terms, and a second term to be verified and to record said procedure in said recording unit; a second program code which makes said processing unit to read out said set of axioms and said set of first terms from said recording unit and to generate, under said set of axioms consisting only of a commutative law and an associative law, a first equational tree automaton which accepts said set of first terms; a third program code which makes said processing unit to read out said set of rewriting rules, said set of axioms and said set of first terms from said recording unit and to generate, under said set of rewriting rules and said set of axioms and using said first equational tree automaton as initial data, a second equational tree automaton which accepts said set of first terms and a set that comprises terms derived from said set of first terms; and a fourth program code which makes said processing unit to determine whether or not said second equational tree automaton accepts said second term to be verified, wherein said second program code makes said processing unit to execute first and second repetition processes; wherein said first repetition process comprises: (A) setting said first equational tree automaton to initial data; (B) selecting an element p from a first group which consists of position information in a tree-structure when left sides of equations, each of said equations corresponding to a rewriting rule in said set of rewriting rules, are described in tree-structure, wherein said element p is positioned at the end of said tree-structure; (C) determining a set of third terms by rewriting all terms which are included in a third equational tree automaton obtained in a last process performed according to the rewriting rule ƒ(c p.l tl , . . . , c p.n tn )-->c p l|p , wherein a function symbol of said element p is described as ƒ, argument terms are described as t l , . . . , t n , and a term l|p corresponding to said element p is described as ƒ(t l , . . . , t n ); (D) obtaining a fourth equational tree automaton by performing repeatedly said (B) selecting and (C) determining processes regarding all elements p positioned at the ends of said tree-structure of said first group; and wherein said second repetition process comprises: (E) setting said fourth equational tree automaton to initial data; (F) selecting an element q from a second group which consists of position information in a tree-structure when right sides of equations, each of said equations corresponding to a rewriting rule in said set of rewriting rules, are described in tree-structure, wherein said element q is positioned at the end of said tree-structure; (G) determining a set of fourth terms by rewriting all terms which are included in a fifth equational tree automaton obtained in a last process performed according to the rewriting rule ƒ(d q.l tl , . . . , d q.n tn )-->d q r|q , wherein a function symbol of said element q is described as ƒ, argument terms are described as t l , . . . , t n , and a term r|q corresponding to said element q is described as ƒ(t l , . . . , t n ); and (H) obtaining said second equational tree automaton by performing repeatedly said (F) selecting and (G) determining processes regarding all elements q positioned at the ends of said tree-structure of said second group.
11. A computer-readable recording medium containing a reactive system safety verification computer program, said reactive system being an electronic system, which is a cipher communication system or control system for a nuclear reactor or aircraft, said computer program being executed by a computer comprising a processing unit and a recording unit, and said computer program comprising: a first program code which makes said processing unit to accept an input of a procedure represented by a set of function symbols, a set of rewriting rules, a set of axioms, a set of first terms, and a second term to be verified and to record said procedure in said recording unit; a second program code which makes said processing unit to read out said set of axioms and said set of first terms from said recording unit and to generate, under said set of axioms consisting only of a commutative law and an associative law, a first equational tree automaton which accepts said set of first terms; a third program code which makes said processing unit to read out said set of rewriting rules, said set of axioms and said set of first terms from said recording unit and to generate, under said set of rewriting rules and said set of axioms and using said first equational tree automaton as initial data, a second equational tree automaton which accepts said set of first terms and a set that comprises terms derived from said set of first terms; and a fourth program code which makes said processing unit to determine whether or not said second equational tree automaton accepts said second term to be verified, wherein said second program code makes said processing unit to execute first and second repetition processes; wherein said first repetition process comprises: (A) setting said first equational tree automaton to initial data; (B) selecting an element p from a first group which consists of position information in a tree-structure when left sides of equations, each of said equations corresponding to a rewriting rule in said set of rewriting rules, are described in tree-structure, wherein said element p is positioned at the end of said tree-structure; (C) determining a set of third terms by rewriting all terms which are included in a third equational tree automaton obtained in a last process performed according to the rewriting rule ƒ(c p.l tl , . . . , c p.n tn )-->c p l|p , wherein a function symbol of said element p is described as ƒ, argument terms are described as t l , . . . , t n , and a term l|p corresponding to said element p is described as ƒ(t l , . . . , t n ); (D) obtaining a fourth equational tree automaton by performing repeatedly said (B) selecting and (C) determining processes regarding all elements p positioned at the ends of said tree-structure of said first group; and wherein said second repetition process comprises: (E) setting said fourth equational tree automaton to initial data; (F) selecting an element q from a second group which consists of position information in a tree-structure when right sides of equations, each of said equations corresponding to a rewriting rule in said set of rewriting rules, are described in tree-structure, wherein said element q is positioned at the end of said tree-structure; (G) determining a set of fourth terms by rewriting all terms which are included in a fifth equational tree automaton obtained in a last process performed according to the rewriting rule ƒ(d q.l tl , . . . , d q.n tn )-->d q r|q , wherein a function symbol of said element q is described as ƒ, argument terms are described as t l , . . . , t n , and a term r|q corresponding to said element q is described as ƒ(t l , . . . , t n ); and (H) obtaining said second equational tree automaton by performing repeatedly said (F) selecting and (G) determining processes regarding all elements q positioned at the ends of said tree-structure of said second group. 12. A computer-readable recording medium containing a reactive system safety verification computer program according to claim 11 , wherein said set of function symbols is a set comprising function symbols representing encryption, decryption and communication processing as elements, said set of rewriting rules is a set comprising as an element a rule representing that encrypted information is returned to plaintext by decryption, said second term to be verified is confidential information, and said set of first terms is a set of knowledge of each of subjects that exchange confidential information, and a set of knowledge of a subject that monitors the information exchanged between said subjects.