Attack on Security Protocol Based on Homomorphism and Its Formal Verification

This paper introduces two attacks on security protocols which have cipher homomorphism, defines term representation and security protocol model based on role's action sequences, proposes a method of transforming role instances interleaving to sequence of constraints, extends the Dolev-Yao intruder model with equational theory, putforwards a intruder deduction system in first-order logic, models and verifies NSL protocol using constraint solving method, discovers the attack based on cipher homomorphism which can not be found under perpect cryptography assumptions.