Gröbner bases are one approach, but you should also explore SAT solvers. For some problem instances, SAT solvers seem to be more effective. There's a straightforward translation of equations over GF(2) to SAT instances.
If you want to try out various SAT solvers, MiniSAT is a good starting point; it is a solid SAT solver that is pretty good. You might be especially intersted in CryptoMiniSAT, which is based upon MiniSAT but is extended to be especially useful for cryptographic problems. In particular, it was extended to be more effective at reasoning about XOR operations, which are common in cryptography (XOR corresponds to addition in GF(2)), though you may have to set a special configuration parameter to enable this support fully. STP is also a convenient tool for this, as it contains a built-in pre-processing that applies Gaussian elimination over GF(2), which can be convenient for some problem instances.
Finally, you could learn about linearization (converting non-linear equations into linear ones, over a larger set of variables) and re-linearization (applying this idea multiple times). This can sometimes be effective if you have a highly over-constrained set of equations over GF(2).
See also http://www.cryptosystem.net/aes/tools.html (but I make no guarantees whether anything there is accurate or useful).