How-To: Infer the protocol's taggings

  1. run PEAR
  2. choose a validation rule system
  3. select the protocol source to be analyzed: you may create a new source or open an existing one; to open an existing source
  4. 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.
  5. you may want to set the logger verbosity (not recommended)
  6. press the open inference dialog button
  7. you may set the inference options as you like
  8. press the run button in the tag inference dialog
  9. if you wish to interrupt the process, then you may press the stop button
  10. 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