In other words, Maude lets us define formally what we mean by some concept in a very abstract manner (not concerning ourselves with how the structure is internally represented and so on), but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules).
Maude lets the user specify whether or not operators are infix, postfix or prefix (default), this is done using underscores as place fillers for the input terms.
A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce.
Maude has the ability to control what rule applications should be attempted at each step using meta-programming, due to the reflective property or rewriting logic.
The Maude system has proved flaws in cryptography protocols by just specifying what the system can do, and by looking for unwanted situations (states or terms that should not be possible to reach) the protocol can be shown to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do.