Symbolically evaluate abstract cryptographic operations
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?