diff --git a/Changelog b/gui/Changelog.txt similarity index 100% rename from Changelog rename to gui/Changelog.txt diff --git a/gui/README.txt b/gui/README.txt index 12e5ae7..968a725 100644 --- a/gui/README.txt +++ b/gui/README.txt @@ -2,14 +2,14 @@ Scyther - 1.0-beta4 + 1.0-beta5 - a automatic verification tool for security protocols + an automatic verification tool for security protocols by Cas Cremers Microsoft Windows binary and - Linux binary compiled for Linux i686 environments + Linux binary (compiled for Linux i686 environments) ------------------------------------------------------------------------ @@ -23,7 +23,7 @@ Note: This is a BETA release, and therefore the usual warnings apply. For more information, see: - http://www.win.tue.nl/~ccremers/scyther + http://people.inf.ethz.ch/cremersc/scyther/index.html 2. Starting out @@ -41,14 +41,11 @@ SPORE directory. 3. Citing Scyther =========================== -For now, there is no official journal paper to cite yet, but you can use -the following information: - -@misc{wwwscyther, - Author = "C.J.F. Cremers", - Title = "The Scyther Tool : Automated Verification of Security Protocols", - Note = "\url{http://www.win.tue.nl/~ccremers/scyther}", - url = "http://www.win.tue.nl/~ccremers/scyther" +@phdthesis{cremers06, + Author = "Cas Cremers", + Title = "Scyther - Semantics and Verification of Security Protocols", + school = "Eindhoven University of Technology", + publisher = "University Press Eindhoven", + year = "2006", } - diff --git a/gui/Scyther/Bin/scyther-linux b/gui/Scyther/Bin/scyther-linux index 543fdeb..2d821db 100755 Binary files a/gui/Scyther/Bin/scyther-linux and b/gui/Scyther/Bin/scyther-linux differ diff --git a/gui/Scyther/Bin/scyther-w32.exe b/gui/Scyther/Bin/scyther-w32.exe index 130063a..8986278 100755 Binary files a/gui/Scyther/Bin/scyther-w32.exe and b/gui/Scyther/Bin/scyther-w32.exe differ diff --git a/gui/mpa.py b/gui/mpa.py index 3cf10a7..a3aff20 100755 --- a/gui/mpa.py +++ b/gui/mpa.py @@ -129,7 +129,7 @@ if __name__ == '__main__': Simple test case with a few protocols """ - list = ['me.spdl','ns3.spdl','nsl3.spdl'] + list = ['nsl3-broken.spdl','ns3.spdl','nsl3.spdl'] print "Performing multi-protocol analysis for the following protocols:", list print findAllMPA(list) diff --git a/gui/nsl3-broken.spdl b/gui/nsl3-broken.spdl new file mode 100644 index 0000000..a0cf88e --- /dev/null +++ b/gui/nsl3-broken.spdl @@ -0,0 +1,52 @@ +/* + * Needham-Schroeder-Lowe protocol, + * broken version (wrong role name in first message) + */ + +// PKI infrastructure + +const pk: Function; +secret sk: Function; +inversekeys (pk,sk); + +// The protocol description + +protocol nsl3-broken(I,R) +{ + role I + { + const ni: Nonce; + var nr: Nonce; + + send_1(I,R, {R,ni}pk(R) ); + read_2(R,I, {ni,nr,R}pk(I) ); + send_3(I,R, {nr}pk(R) ); + + claim_i1(I,Secret,ni); + claim_i2(I,Secret,nr); + claim_i3(I,Niagree); + claim_i4(I,Nisynch); + } + + role R + { + var ni: Nonce; + const nr: Nonce; + + read_1(I,R, {R,ni}pk(R) ); + send_2(R,I, {ni,nr,R}pk(I) ); + read_3(I,R, {nr}pk(R) ); + + claim_r1(R,Secret,ni); + claim_r2(R,Secret,nr); + claim_r3(R,Niagree); + claim_r4(R,Nisynch); + } +} + +// An untrusted agent, with leaked information + +const Eve: Agent; +untrusted Eve; +compromised sk(Eve); +