Attack Editor How To

Naming your attack

The upper box labeled "Attack Name" is where you type in the attack name. (Only letters and numbers please, no spaces.). A name is required to either view the attack, or add the new attack to the attack list.

Caveat: If you give an attack a name that is already used it will overwrite the existing attack by that name.

The Term Algebra

The left pane shows the sort hierarchy,the term algebra and the terms your have defined so far (the term pool). These are informational, and are not required to manipulate the contents of the attack. Though you can use the "Add Term" button to practice constructing terms using the new term editor, and adding them to the pool.

The Term Editor

The main new feature of the AttackEditor is the appearance of the term editor. Which allows for the construction of well typed terms of a particular sort. This feature is used:

In its full generality you would be first asked to select a sort, though in some of its uses in the AttackEditor, the sort is predetermined by the context. To select a sort you use the combobox provided. This will then populate the "term window" with a sorted hole. To fill that hole, one simply selects it, by clicking on it, and using the combobox. You can either select a constructor or term from the pool (they appear in the dropdown), or else type in the name of a variable, and hit return. If for some reason you which to declare your variable to be a subsort of the sort of the hole, you should simply type the name of the variable, a ":", and then the desired sort. Maude does not know anything about holes, so you should make sure that all the terms you construct are holeless. When you are editing a preexisiting term, you can select any subterm and replace it by another, again by using the combobox, either to choose a template, or enter a variable name.

Adding a role

The second pane from the left is called the "Roles panel" shows the strands of the protocol roles. The rightmost pane is where you specify attack strands, intruder knowledge, and never patterns.

The roles are essentially tabs, and so only one can be visible (or selected) at any one time. These roles can be edited, cloned, and created by using the combobox on the lower right hand side of the roles panel. Editing is done by way of a popup dialog for that purpose. A role consists of a name, a set of fresh variables, and a list of terms. To add terms to the list one uses the "+" button. Selecting the newly added hole, and completeing it as desired using the term editor. The rows in the role editor can be reordered by dragging and dropping. Deleting a row can be done by selecting it and then using the "-" button. To select it without launching the term editor for that cell, simple check the box marked "Select only".

If you select a role you will be offered the opportunity to add an instance of the role to the attack, or to a never pattern, again by using the combobox associated with the roles panel. You can then use the table to edit the appropriate values. For example, you can specify the intial segment of the strand (default is the full strand), the position of the bar (default is at the end), fresh names (default is those declared for the role) and the substitution for the instance (default is the identity). To change the position of the bar or the strand height click on the number in the "Bar" or "Height" column and select the desired number. To change the fresh set, click on the text in the "Fresh" column and type in fresh variable names. (They will automatially be given sort "Fresh"). To modify the default substitution, click in the "Substitution" column (in the row of the strand you are working on). A "Substitution Dialog" will appear, listing the variables, their sorts, and the current binding. Click on the value and use the launched term editor to change this value.

Adding intruder knowledge

To specify intruder knowledge for the attack, click on the "+" button and use the term editor. As like in the role editor, rows can be deleted by selecting them and using the "-" button.

Committing your Attack

Once you are happy with the attack press the OK button (lower right). If you have not filled in the name, you will be prompted to do so. The attack will be added to the list in the manager window, where you can select and "Accept" it just like the pre-defined attacks.

When you are done editing, just close the editor window. Pressing "Edit Attack" will bring it back, in the state you left it. You can delete strands or intruder knowledge to make a new attack.