Monday, January 6, 2020

Running Scyther Tool v1.1.3 on Mac OS X Catalina

The Scyther tool is a relatively simple protocol verification tool which performs formal verification of any security protocols. Although it may not be as powerful as Tamarin Prover, its relatively simple scripting language and GUI interface help learners to kick-start their project easily.

The Scyther tool should run seamlessly on older versions of Mac because of the older version of wxPython. However since Catalina, the libraries should have been updated, causing some issues while running the program.

Here explained some changes after my experiments:

1. Download Scyther Tool for Mac v1.1.3 here:
https://people.cispa.io/cas.cremers/scyther/index.html

2. Unzip and navigate to the terminal

3. run the following command:
python scyther-gui.py

4. Run some examples such as NSPK:
https://github.com/cascremers/scyther/blob/master/gui/Protocols/needham-schroeder.spdl

5. Check if you experienced some errors like this:
  File "/Users/chriz/Desktop/scyther-mac-v1.1.3/Gui/Attackwindow.py", line 96, in update
    (framewidth,frameheight) = self.GetClientSizeTuple()
AttributeError: 'AttackDisplay' object has no attribute 'GetClientSizeTuple'

  File "/Users/chriz/Desktop/scyther-mac-v1.1.3/Gui/Attackwindow.py", line 121, in update
    if not bmp.Ok():
AttributeError: 'Image' object has no attribute 'Ok'

If so, change the following two lines in Gui/Attackwindow.py:

Line 96:
- (framewidth,frameheight) = self.GetClientSizeTuple()
+ (framewidth,frameheight) = self.GetClientSize()
Line 121:
- if not bmp.Ok():
+ if not bmp.IsOk():

6. After modifying the code above, re-run the Step 3.
Although there are still some other errors, it should at least run with patterns successfully shown.

Screen Capture:


---

Reference:

https://wxpython.org/Phoenix/docs/html/classic_vs_phoenix.html
https://wxpython.org/Phoenix/docs/html/wx.Image.html