next up previous
Next: Queries for Finding Known Up: Notation and Rewrite Rules Previous: Notation

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