Rewrite Rules

Here we give a set of rewrite rules that describe the relationship between encryption and decryption. These are the rules that will be used by the Analyzer to model the effects of encryption and decryption.

ecbc(K,IV,dcbc(K,IV,C))$\rightarrow$ C
dcbc(K,IV,ecbc(K,IV,P))$\rightarrow$ P