Symbolically evaluate abstract cryptographic operations

edit

I would like to use simple variable substitution to show some basic properties of cryptographic constructions using Sage. For example, I want to define an encrpytion and decryption function E and D, so that for a given message m and key k

D(E(m, k), k) = m

I.e., the decrypted encrypted message is the message.

Furthermore, I want to specify that all those variables, (m, k in the above example) are vectors in GF(2) of length 128. This would allow me to use XOR so that

m + m = vector(GF(2), 128)

I.e., a block XOR itself is zero.

I cannot find a way to do this properly (i.e., that XOR terms that cancel each other out are simplified away and that I can use symbolic "encryption" function blocks). Is this possible somehow?