Obfuscated Dechiper Routine Analysis Using Theorem Prover for Information Protection

Information leak has been increasing, which imposes a great burden on IT business. Software protection and trusted computing are promising technologies to cope with malicious or illegal access to mission-critical servers. Code obfuscation and encryption are important techniques for software protection. In this paper, we present an obfuscated decipher routine analysis using theorem prover. For detecting parameters of decipher routine, we apply equality substitution techniques called paramodulation and demodulation. Besides, we apply look-ahead strategies to speed up our analysis. Experimental result shows that FoL theorem prover works well for analyzing obfuscated decipher routine, particularly detecting parameters. Theorem prover is effective tool for enhancing information protection.