How-To: Infer the protocol's taggings
- run PEAR
- choose a validation rule system
- select the protocol source to be analyzed: you may
create a new source or open an existing one;
to open an existing source
- if the protocol source is untagged
and it's the first time you try to infer its taggings, you'll have to
label the encryption-decryption couples:
- switch to the source editing mode
- locate the first encryption (decryption) primitive
you can find
- type a label followed by a colon just before it,
for example:
a:
encrypt
{A, n, M} as x.
- locate the corresponding decryption (encryption)
primitive
- type the same label as before, for example:
a:
decrypt y as {A, x, z}.
- switch to the source displaying mode (the modified
source will be syntax-checked)
note: only labeled primitives will be tagged.
- you may want to set the logger
verbosity (not recommended)
- press the open inference
dialog button
- you may set the inference
options as you like
- press the run button in the tag inference dialog
- if you wish to interrupt the process, then you may press
the stop button
- when the process completes, the title bar reports the number of taggings
found; to save each of them:
- choose the tagging you wish to save through the
above selector
- press the save button, a file choose will be displayed
- choose the target path and file name
- press the save button in the file chooser dialog