We present a methodology to automatically construct robust signatures whose accuracy is based on formal reasoning so it can be systematically evaluated.Our methodology is based on two formal languages that describe different properties of a given attack. The first language, called a session signature, describes temporal relations between the attack events. The second, called an attack invariant, describes semantic properties that hold in any instance of the attack. For example, an invariant may state that a given FTP attack must include a successful FTP login and can be launched only after the FTP representation mode has been set to ASCII. We iteratively eliminate false positives and negatives from an initial session signature by comparing the signature language to the language of the invariant.We developed GARD, a tool for session-signature construction, and used it to construct session signatures for multi-step attacks. We show that a session signature is more accurate than existing signatures.