Attack on Security Protocol Based on Homomorphism and Its Formal Verification
Yadi Wang · Jisuanji gongcheng · 2009
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.