Radio communication is vital for satellite and rocket control, demanding the highest security to ensure public safety. While traditional systems rely on computational security, advancements in COTS electronics have made information-theoretic security practical for spacecraft radio links, comparable to quantum key distribution (QKD). Authentication based on finite field multiplication over \(GF(2^n)\) requires compact, combinational circuits for speed and radiation resistance, with formal verification ensuring design correctness. For \(n=128\) , the composite field \(GF(((((((2^2)^2)^2)^2)^2)^2)^2)\) , built through seven extensions, achieves minimal circuit size. However, dynamic verification struggles with exhaustive testing and correct test data generation. This paper proposes a formal verification method using finite field isomorphism and AND-XOR logic equivalence checking. A simplified reference circuit based on a single extension \(GF(2^{128})\) improves verification efficiency. The method successfully verified a circuit implementation for \(n=128\) (input space \(2^{256}\) ) within a day of runtime.