From 47c9a6694dfd6af7bbaa05f9e8141a28bb6ecdab Mon Sep 17 00:00:00 2001 From: Andrew Date: Thu, 14 May 2015 22:00:32 -0500 Subject: [PATCH] Now that I've finished updating all the PSL files, I've moved all the PSL files back into the normal examples folder. --- .../Amended-Needham-Schroeder.psl | 0 examples/{done_examples => }/Carlsen-SK.psl | 0 .../{done_examples => }/Denning-Sacco.psl | 0 examples/{done_examples => }/ISO5.psl | 0 examples/{done_examples => }/Kao-Chow.psl | 0 examples/{done_examples => }/Otway-Rees.psl | 0 examples/{done_examples => }/Woolam.psl | 0 examples/Yahalom.psl | 94 +++++++------ examples/{done_examples => }/db.psl | 0 examples/{done_examples => }/dh.psl | 0 .../Amended-Needham-Schroeder.maude | 120 ----------------- examples/done_examples/Otway-Rees-command | 18 --- examples/done_examples/Otway-Rees.maude | 123 ------------------ examples/done_examples/nspk-command | 29 ----- examples/done_examples/nspk.maude | 90 ------------- examples/done_examples/nspk.pslmaude | 56 -------- examples/{done_examples => }/kd.psl | 0 examples/{done_examples => }/nsl.psl | 0 examples/{done_examples => }/nspk.psl | 0 examples/{done_examples => }/wmf.psl | 0 20 files changed, 44 insertions(+), 486 deletions(-) rename examples/{done_examples => }/Amended-Needham-Schroeder.psl (100%) rename examples/{done_examples => }/Carlsen-SK.psl (100%) rename examples/{done_examples => }/Denning-Sacco.psl (100%) rename examples/{done_examples => }/ISO5.psl (100%) rename examples/{done_examples => }/Kao-Chow.psl (100%) rename examples/{done_examples => }/Otway-Rees.psl (100%) rename examples/{done_examples => }/Woolam.psl (100%) rename examples/{done_examples => }/db.psl (100%) rename examples/{done_examples => }/dh.psl (100%) delete mode 100644 examples/done_examples/Amended-Needham-Schroeder.maude delete mode 100755 examples/done_examples/Otway-Rees-command delete mode 100644 examples/done_examples/Otway-Rees.maude delete mode 100755 examples/done_examples/nspk-command delete mode 100644 examples/done_examples/nspk.maude delete mode 100644 examples/done_examples/nspk.pslmaude rename examples/{done_examples => }/kd.psl (100%) rename examples/{done_examples => }/nsl.psl (100%) rename examples/{done_examples => }/nspk.psl (100%) rename examples/{done_examples => }/wmf.psl (100%) diff --git a/examples/done_examples/Amended-Needham-Schroeder.psl b/examples/Amended-Needham-Schroeder.psl similarity index 100% rename from examples/done_examples/Amended-Needham-Schroeder.psl rename to examples/Amended-Needham-Schroeder.psl diff --git a/examples/done_examples/Carlsen-SK.psl b/examples/Carlsen-SK.psl similarity index 100% rename from examples/done_examples/Carlsen-SK.psl rename to examples/Carlsen-SK.psl diff --git a/examples/done_examples/Denning-Sacco.psl b/examples/Denning-Sacco.psl similarity index 100% rename from examples/done_examples/Denning-Sacco.psl rename to examples/Denning-Sacco.psl diff --git a/examples/done_examples/ISO5.psl b/examples/ISO5.psl similarity index 100% rename from examples/done_examples/ISO5.psl rename to examples/ISO5.psl diff --git a/examples/done_examples/Kao-Chow.psl b/examples/Kao-Chow.psl similarity index 100% rename from examples/done_examples/Kao-Chow.psl rename to examples/Kao-Chow.psl diff --git a/examples/done_examples/Otway-Rees.psl b/examples/Otway-Rees.psl similarity index 100% rename from examples/done_examples/Otway-Rees.psl rename to examples/Otway-Rees.psl diff --git a/examples/done_examples/Woolam.psl b/examples/Woolam.psl similarity index 100% rename from examples/done_examples/Woolam.psl rename to examples/Woolam.psl diff --git a/examples/Yahalom.psl b/examples/Yahalom.psl index f234774..91f3381 100644 --- a/examples/Yahalom.psl +++ b/examples/Yahalom.psl @@ -1,15 +1,15 @@ spec Yahalom is Theory - types Uname Sname name Key Nonce Masterkey Sessionkey . + types Uname Sname Name Key Nonce Masterkey Sessionkey . subtype Masterkey Sessionkey < Key . - subtype Sname Uname < name . - subtype name < Public . + subtype Sname Uname < Name . + subtype Name < Public . - op n : name Fresh -> Nonce . + op n : Name Fresh -> Nonce . ops a b i : -> Uname [ctor] . op s : -> Sname [ctor] . - op mkey : name name -> Masterkey . - op seskey : name name Nonce -> Sessionkey . + op mkey : Name Name -> Masterkey . + op seskey : Name Name Nonce -> Sessionkey . op e : Key Msg -> Msg . op d : Key Msg -> Msg . op _;_ : Msg Msg -> Msg [gather (e E)] . @@ -25,74 +25,68 @@ Theory A -> B : E(kbs:A,kab),E(kab:nb) */ -/* -Note: The variable scoping here makes no sense. Ostensibly, the SK in Protocol, and the SK in Attacks should be different values. However, they're meant to represent the same -value. So, it seems like we should allow global variable declarations. Of course, the way the code is currently structured, implementing that won't exactly be trivial. - -*/ Protocol - vars A B : Uname . - var S : Sname . - vars NA NB : Nonce . + vars ANAME BNAME : Uname . + var SNAME : Sname . + vars NA NBA NAS NBS : Nonce . var r : Fresh . var M N MB : Msg . - var SK : Sessionkey . - var D : name . + var SKA SKB : Sessionkey . + var D : Name . var K : Key . - Def(A) = na := n(A, r), kas := mkey(A,s) . - In(A) = A, B, S . + roles A B S . + + In(A) = ANAME, BNAME, SNAME . + In(B) = ANAME, BNAME, SNAME . + In(S) = ANAME, BNAME, SNAME . + + Def(A) = na := n(ANAME, r), kas := mkey(ANAME,s) . - Def(B) = nb := n(B, r), kbs := mkey(B,s) . - In(B) = A, B, S . + Def(B) = nb := n(BNAME, r), kbs := mkey(BNAME,s) . - Def(S) = kas := mkey(A, s), kbs := mkey(B, s), kab := seskey(A , B , n(s,r)) . - In(S) = A, B, S . + Def(S) = kas := mkey(ANAME, s), kbs := mkey(BNAME, s), + kab := seskey(ANAME , BNAME , n(s,r)) . - 1 . A -> B : A ; na - |- A ; NA . + 1 . A -> B : ANAME ; na + |- ANAME ; NA . - 2 . B -> S : B ; e(kbs, A ; NA ; nb) - |- B ; e(kbs, A ; NA ; NB) . + 2 . B -> S : BNAME ; e(kbs, ANAME ; NA ; nb) + |- BNAME ; e(kbs, ANAME ; NAS ; NBS) . - 3 . S -> A : e(kas, B ; kab ; NA ; NB) ; e(kbs, A ; kab) - |- e(kas, B ; SK ; na ; NB) ; MB . + 3 . S -> A : e(kas, BNAME ; kab ; NAS ; NBS) ; e(kbs, ANAME ; kab) + |- e(kas, BNAME ; SKA ; na ; NBA) ; MB . - 4 . A -> B : MB ; e(SK, NB) - |- e(kbs, A ; SK) ; e(SK, nb) . + 4 . A -> B : MB ; e(SKA, NBA) + |- e(kbs, ANAME ; SKB) ; e(SKB, nb) . - Out(A) = na, NB, SK . - Out(B) = NA, nb, SK . - Out(S) = NA, NB, kab . + Out(A) = na, NBA, SKA . + Out(B) = NA, nb, SKB . + Out(S) = NA, NBS, kab . Intruder - => D:Name, n(i, r:Fresh), mkey(i, A:Name), mkey(A:Name, i), mkey(i, s) . - K:Key, M:Msg => d(K:Key, M:Msg), e(K:Key, M:Msg) . - M:Msg ; N:Msg <=> M:Msg, N:Msg . + vars C D : Name . + var r : Fresh . + var K : Key . + vars M N : Msg . + => D, n(i, r), mkey(i, C), mkey(C, i), mkey(i, s) . + K, M => d(K, M), e(K, M) . + M ; N <=> M, N . Attacks - vars A B : UName . - var S : SName . - var SK : Sessionkey . - 0 . - In(B) = A |-> a , B |-> b, S |-> s . B executes protocol . - Out(B) = ditto . + Subst(B) = ANAME |-> a , BNAME |-> b, SNAME |-> s . 1 . - In(B) = A |-> a , B |-> b, S |-> s . B executes protocol . - Intruder learns SK . - Out(B) = ditto . + Subst(B) = ANAME |-> a , BNAME |-> b, SNAME |-> s . + Intruder learns SKB . 2 . - In(B) = A |-> a, B |-> b, S |-> s . B executes protocol . - Out(B) = ditto . + Subst(B) = ANAME |-> a, BNAME |-> b, SNAME |-> s . without: - In(A) = A |-> a, B |-> b, S |-> s . A executes protocol . - Out(A) = NB |-> n(b, r), ditto . - + Subst(A) = ANAME |-> a, BNAME |-> b, SNAME |-> s, NBA |-> n(b, r) . ends diff --git a/examples/done_examples/db.psl b/examples/db.psl similarity index 100% rename from examples/done_examples/db.psl rename to examples/db.psl diff --git a/examples/done_examples/dh.psl b/examples/dh.psl similarity index 100% rename from examples/done_examples/dh.psl rename to examples/dh.psl diff --git a/examples/done_examples/Amended-Needham-Schroeder.maude b/examples/done_examples/Amended-Needham-Schroeder.maude deleted file mode 100644 index e08804f..0000000 --- a/examples/done_examples/Amended-Needham-Schroeder.maude +++ /dev/null @@ -1,120 +0,0 @@ -fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . -sorts SName Name Key Nonce Masterkey Sessionkey . -subsorts Masterkey Sessionkey < Key . -subsorts SName < Name . -subsorts Name < Public . -op n : Name Fresh -> Nonce [ frozen ] . -op a : -> Name . -op b : -> Name . -op i : -> Name . -op s : -> SName . -op mkey : Name Name -> Masterkey [ frozen ] . -op seskey : Name Name Nonce -> Sessionkey [ frozen ] . -op e : Key Msg -> Msg [ frozen ] . -op d : Key Msg -> Msg [ frozen ] . -op dec : Nonce -> Msg [ frozen ] . -op null : -> Msg . -op _;_ : Msg Msg -> Msg [ gather ( e E ) frozen ] . -op t : -> Msg . -subsorts SName Name Key Nonce Masterkey Sessionkey < Msg . -op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen]. -endfm - -fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS . -eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg [ variant ] . -eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg [ variant ] . -endfm -fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS . -protecting DEFINITION-PROTOCOL-RULES . -protecting DEFINITION-CONSTRAINTS-INPUT . -eq STRANDS-DOLEVYAO = -:: nil :: -[ nil | - +(s), nil] & -:: nil :: -[ nil | - +(A:Name), nil] & -:: nil :: -[ nil | - +(mkey(i, s)), nil] & -:: nil :: -[ nil | - +(mkey(i, A:Name)), nil] & -:: nil :: -[ nil | - +(mkey(s, i)), nil] & -:: nil :: -[ nil | - +(mkey(A:Name, i)), nil] & -:: nil :: -[ nil | - -(M1:Msg), - -(M:Msg), - +(M:Msg ; M1:Msg), nil] & -:: nil :: -[ nil | - -(N:Nonce), - +(dec(N:Nonce)), nil] & -:: nil :: -[ nil | - -(K:Key), - -(M:Msg), - +(e(K:Key, M:Msg)), nil] & -:: nil :: -[ nil | - -(K:Key), - -(M:Msg), - +(d(K:Key, M:Msg)), nil] & -:: nil :: -[ nil | - -(dec(N:Nonce)), - +(N:Nonce), nil] & -:: nil :: -[ nil | - -(M:Msg ; M1:Msg), - +(M:Msg), nil] & -:: nil :: -[ nil | - -(M:Msg ; M1:Msg), - +(M1:Msg), nil] & -:: r:Fresh :: -[ nil | - +(n(i, r:Fresh)), nil] [nonexec]. -eq STRANDS-PROTOCOL = -:: r:Fresh :: -[ nil | - +(ANAME:Name), - -(M1:Msg), - +(ANAME:Name ; BNAME:Name ; n(ANAME:Name, r:Fresh) ; M1:Msg), - -(e(mkey(ANAME:Name, SNAME:Name), n(ANAME:Name, r:Fresh) ; BNAME:Name ; KA:Key ; M2:Msg)), - +(M2:Msg), - -(e(KA:Key, NB:Nonce)), - +(e(KA:Key, dec(NB:Nonce))), nil] & -:: r1:Fresh :: -[ nil | - -(A2NAME:Name ; B2NAME:Name ; NA2:Nonce ; e(mkey(B2NAME:Name, SNAME:Name), A2NAME:Name ; NB2:Nonce)), - +(e(mkey(A2NAME:Name, SNAME:Name), NA2:Nonce ; B2NAME:Name ; seskey(A2NAME:Name, B2NAME:Name, n(SNAME:Name, r1:Fresh)) ; e(mkey(B2NAME:Name, SNAME:Name), seskey(A2NAME:Name, B2NAME:Name, n(SNAME:Name, r1:Fresh)) ; NB2:Nonce ; A2NAME:Name))), nil] & -:: r2:Fresh,r0:Fresh :: -[ nil | - -(A1NAME:Name), - +(e(mkey(BNAME:Name, SNAME:Name), A1NAME:Name ; n(BNAME:Name, r0:Fresh))), - -(e(mkey(BNAME:Name, SNAME:Name), KB:Key ; n(BNAME:Name, r0:Fresh) ; A1NAME:Name)), - +(e(KB:Key, n(BNAME:Name, r2:Fresh))), - -(e(KB:Key, dec(n(BNAME:Name, r2:Fresh)))), nil] [nonexec]. -var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)= -:: r2:Fresh,r0:Fresh :: -[ nil, - -(a), - +(e(mkey(b, s), a ; n(b, r0:Fresh))), - -(e(mkey(b, s), KB:Key ; n(b, r0:Fresh) ; a)), - +(e(KB:Key, n(b, r2:Fresh))), - -(e(KB:Key, dec(n(b, r2:Fresh)))) | nil] -|| empty -|| -nil -|| -nil -|| -nil[nonexec]. - endfm -select MAUDE-NPA . \ No newline at end of file diff --git a/examples/done_examples/Otway-Rees-command b/examples/done_examples/Otway-Rees-command deleted file mode 100755 index 24a5a32..0000000 --- a/examples/done_examples/Otway-Rees-command +++ /dev/null @@ -1,18 +0,0 @@ -date -#!/bin/bash -./maude27 -no-prelude prelude.maude < Nonce [ frozen ] . -ops a b i : -> UName . -op s : -> SName . -op mkey : Name Name -> Masterkey [ frozen ] . -op seskey : Name Name Nonce -> Sessionkey [ frozen ] . -op e : Key Msg -> Msg [ frozen ] . -op d : Key Msg -> Msg [ frozen ] . -op _;_ : Msg Msg -> Msg [ gather ( e E ) frozen ] . -subsorts UName SName Name Key Nonce Masterkey Sessionkey < Msg . -op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen]. -endfm - -fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS . -eq d(K:Key, e(K:Key, Z:Msg)) = Z:Msg [ variant ] . -eq e(K:Key, d(K:Key, Z:Msg)) = Z:Msg [ variant ] . -endfm -fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS . -protecting DEFINITION-PROTOCOL-RULES . -protecting DEFINITION-CONSTRAINTS-INPUT . -eq STRANDS-DOLEVYAO = -:: nil :: -[ nil | - +(s), nil] & -:: nil :: -[ nil | - +(P:UName), nil] & -:: nil :: -[ nil | - +(mkey(i, s)), nil] & -:: nil :: -[ nil | - -(M:Msg), - -(N:Msg), - +(M:Msg ; N:Msg), nil] & -:: nil :: -[ nil | - -(P:UName), - +(mkey(i, P:UName)), nil] & -:: nil :: -[ nil | - -(P:UName), - +(mkey(P:UName, i)), nil] & -:: nil :: -[ nil | - -(K:Key), - -(M:Msg), - +(e(K:Key, M:Msg)), nil] & -:: nil :: -[ nil | - -(K:Key), - -(M:Msg), - +(d(K:Key, M:Msg)), nil] & -:: nil :: -[ nil | - -(M:Msg ; N:Msg), - +(N:Msg), nil] & -:: nil :: -[ nil | - -(M:Msg ; N:Msg), - +(M:Msg), nil] [nonexec]. -eq STRANDS-PROTOCOL = -:: r':Fresh :: -[ nil | - -(CB:Nonce ; ANAME:UName ; BNAME:UName ; M1:Msg), - +(CB:Nonce ; ANAME:UName ; BNAME:UName ; M1:Msg ; e(mkey(BNAME:UName, SNAME:SName), n(BNAME:UName, r':Fresh) ; CB:Nonce ; ANAME:UName ; BNAME:UName)), - -(CB:Nonce ; MA:Msg ; e(mkey(BNAME:UName, SNAME:SName), n(BNAME:UName, r':Fresh) ; KCB:Sessionkey)), - +(CB:Nonce ; MA:Msg), nil] & -:: r'':Fresh :: -[ nil | - -(CS:Nonce ; ANAME:UName ; BNAME:UName ; e(mkey(ANAME:UName, SNAME:SName), RA:Nonce ; CS:Nonce ; ANAME:UName ; BNAME:UName) ; e(mkey(BNAME:UName, SNAME:SName), RB:Nonce ; CS:Nonce ; ANAME:UName ; BNAME:UName)), - +(CS:Nonce ; e(mkey(ANAME:UName, SNAME:SName), RA:Nonce ; seskey(ANAME:UName, BNAME:UName, n(SNAME:SName, r'':Fresh))) ; e(mkey(BNAME:UName, SNAME:SName), RB:Nonce ; seskey(ANAME:UName, BNAME:UName, n(SNAME:SName, r'':Fresh)))), nil] & -:: r:Fresh,rM:Fresh :: -[ nil | - +(n(ANAME:UName, rM:Fresh) ; ANAME:UName ; BNAME:UName ; e(mkey(ANAME:UName, SNAME:SName), n(ANAME:UName, r:Fresh) ; n(ANAME:UName, rM:Fresh) ; ANAME:UName ; BNAME:UName)), - -(n(ANAME:UName, rM:Fresh) ; e(mkey(ANAME:UName, SNAME:SName), n(ANAME:UName, r:Fresh) ; KCA:Sessionkey)), nil] [nonexec]. -var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)= -:: r:Fresh,rM:Fresh :: -[ nil, - +(n(a, rM:Fresh) ; a ; b ; e(mkey(a, s), n(a, r:Fresh) ; n(a, rM:Fresh) ; a ; b)), - -(n(a, rM:Fresh) ; e(mkey(a, s), n(a, r:Fresh) ; KCA:Sessionkey)) | nil] -|| empty -|| -nil -|| -nil -|| -nil[nonexec]. - eq ATTACK-STATE(1)= -:: r:Fresh,rM:Fresh :: -[ nil, - +(n(a, rM:Fresh) ; a ; b ; e(mkey(a, s), n(a, r:Fresh) ; n(a, rM:Fresh) ; a ; b)), - -(n(a, rM:Fresh) ; e(mkey(a, s), n(a, r:Fresh) ; KCA:Sessionkey)) | nil] -|| -KCA:Sessionkey inI -|| -nil -|| -nil -|| -nil[nonexec]. - eq ATTACK-STATE(2)= -:: r:Fresh,rM:Fresh :: -[ nil, - +(n(a, rM:Fresh) ; a ; b ; e(mkey(a, s), n(a, r:Fresh) ; n(a, rM:Fresh) ; a ; b)), - -(n(a, rM:Fresh) ; e(mkey(a, s), n(a, r:Fresh) ; KCA:Sessionkey)) | nil] -|| empty -|| -nil -|| -nil -|| never((S & -:: r':Fresh :: -[ nil, - -(CB:Nonce ; a ; b ; e(mkey(a, s), n(a, rM:Fresh) ; n(a, r:Fresh) ; a ; b)), - +(CB:Nonce ; a ; b ; e(mkey(a, s), n(a, rM:Fresh) ; n(a, r:Fresh) ; a ; b) ; e(mkey(b, s), n(b, r':Fresh) ; CB:Nonce ; a ; b)), - -(CB:Nonce ; MA:Msg ; e(mkey(b, s), n(b, r':Fresh) ; KCB:Sessionkey)), - +(CB:Nonce ; MA:Msg) | nil] ) || K)[nonexec]. - endfm -select MAUDE-NPA . \ No newline at end of file diff --git a/examples/done_examples/nspk-command b/examples/done_examples/nspk-command deleted file mode 100755 index b194339..0000000 --- a/examples/done_examples/nspk-command +++ /dev/null @@ -1,29 +0,0 @@ -date -#!/bin/bash -./maude27 -no-prelude prelude.maude < Enc [ frozen ] . -op sk : Name Msg -> Enc [ frozen ] . -op n : Name Fresh -> Nonce [ frozen ] . -op _;_ : Msg Msg -> Msg [ ctor gather ( e E ) frozen ] . -ops a b i : -> Name [ ctor ] . -subsorts Name Nonce Enc < Msg . -op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen]. -endfm - -fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS . -eq sk(X:Name, pk(X:Name, Z:Msg)) = Z:Msg [ variant ] . -eq pk(X:Name, sk(X:Name, Z:Msg)) = Z:Msg [ variant ] . -endfm -fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS . -protecting DEFINITION-PROTOCOL-RULES . -protecting DEFINITION-CONSTRAINTS-INPUT . -eq STRANDS-DOLEVYAO = -:: nil :: -[ nil | - -(X:Msg), - +(sk(i, X:Msg)), nil] & -:: nil :: -[ nil | - -(Y:Msg), - -(X:Msg), - +(X:Msg ; Y:Msg), nil] & -:: nil :: -[ nil | - -(A:Name), - -(X:Msg), - +(pk(A:Name, X:Msg)), nil] & -:: nil :: -[ nil | - -(X:Msg ; Y:Msg), - +(X:Msg), nil] & -:: nil :: -[ nil | - -(X:Msg ; Y:Msg), - +(Y:Msg), nil] & -:: r1:Fresh :: -[ nil | - +(n(i, r1:Fresh)), nil] [nonexec]. -eq STRANDS-PROTOCOL = -:: r1:Fresh :: -[ nil | - +(pk(BName:Name, AName:Name ; n(AName:Name, r1:Fresh))), - -(pk(AName:Name, n(AName:Name, r1:Fresh) ; N2:Nonce)), - +(pk(BName:Name, N2:Nonce)), nil] & -:: r2:Fresh :: -[ nil | - -(pk(BName:Name, AName:Name ; N1:Nonce)), - +(pk(AName:Name, N1:Nonce ; n(BName:Name, r2:Fresh))), - -(pk(BName:Name, n(BName:Name, r2:Fresh))), nil] [nonexec]. -var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)= -:: r2:Fresh :: -[ nil, - -(pk(b, a ; N1:Nonce)), - +(pk(a, N1:Nonce ; n(b, r2:Fresh))), - -(pk(b, n(b, r2:Fresh))) | nil] -|| -n(b, r2:Fresh) inI -|| -nil -|| -nil -|| -nil[nonexec]. - eq ATTACK-STATE(1)= -:: r2:Fresh :: -[ nil, - -(pk(b, a ; N1:Nonce)), - +(pk(a, N1:Nonce ; n(b, r2:Fresh))), - -(pk(b, n(b, r2:Fresh))) | nil] -|| -n(b, r2:Fresh) inI -|| -nil -|| -nil -|| never((S & -:: r1:Fresh :: -[ nil, - +(pk(b, a ; n(a, r1:Fresh))), - -(pk(a, n(a, r1:Fresh) ; N2:Nonce)), - +(pk(b, N2:Nonce)) | nil] ) || K)[nonexec]. - endfm -select MAUDE-NPA . \ No newline at end of file diff --git a/examples/done_examples/nspk.pslmaude b/examples/done_examples/nspk.pslmaude deleted file mode 100644 index 0ebd751..0000000 --- a/examples/done_examples/nspk.pslmaude +++ /dev/null @@ -1,56 +0,0 @@ -mod nspk is -protecting TRANSLATION-TO-MAUDE-NPA . -protecting PROTOCOL-EXAMPLE-SYMBOLS . -op pk : Msg Msg -> Enc [frozen] . -op sk : Msg Msg -> Enc [frozen] . -op n : Msg Msg -> Nonce [frozen] . -op _;_ : Msg Msg -> Msg [ctor gather ( e E ) frozen ] . -op a : -> Name [ctor] . -op b : -> Name [ctor] . -op c : -> Name [ctor] . -op i : -> Name [ctor] . -op na : -> Msg . -op nb : -> Msg . -endm -rew -( -Specification { - -Protocol -{ -In ( A:Name ) = A:Name , B:Name .[53] -In ( B:Name ) = A:Name , B:Name .[67] -1 . A:Name -> B:Name : pk ( B:Name , A:Name ; na ) |- pk ( B:Name , A:Name ; N1:Nonce ) .[70] -2 . B:Name -> A:Name : pk ( A:Name , N1:Nonce ; nb ) |- pk ( A:Name , na ; N2:Nonce ) .[71] -3 . A:Name -> B:Name : pk ( B:Name , N2:Nonce ) |- pk ( B:Name , nb ) .[72] -Out ( A:Name ) = na , N2:Nonce .[74] -Out ( B:Name ) = nb , N1:Nonce .[75] -} -Intruder -{ -=> n ( i , r1:Fresh ) .[93] -X:Msg ; Y:Msg <=> X:Msg , Y:Msg .[94] -X:Msg => sk ( i , X:Msg ) .[95] -X:Msg , A:Name => pk ( A:Name , X:Msg ) .[96] -} -Attacks -{ -{ In ( B:Name ) = A:Name |-> a , B:Name |-> b .[112] -B:Name executes protocol .[116] -Intruder learns nb .[120] -Out ( B:Name ) = ditto .[139] -{ In ( B:Name ) = A:Name |-> a , B:Name |-> b .[141] -B:Name executes protocol .[142] -Intruder learns nb .[143] -Out ( B:Name ) = ditto .[144] -without: In ( A:Name ) = A:Name |-> a , B:Name |-> b .[157] -A:Name executes protocol .[159] -Out ( A:Name ) = ditto .[160] -} -} -[na := n ( A:Name , r1:Fresh ), nb := n ( B:Name , r2:Fresh ), $noDefs] -[(mt).StrandData] -[(empty).StrandSet] -{##K##:IntruderKnowledge} -{##S##:StrandSet}) . -q \ No newline at end of file diff --git a/examples/done_examples/kd.psl b/examples/kd.psl similarity index 100% rename from examples/done_examples/kd.psl rename to examples/kd.psl diff --git a/examples/done_examples/nsl.psl b/examples/nsl.psl similarity index 100% rename from examples/done_examples/nsl.psl rename to examples/nsl.psl diff --git a/examples/done_examples/nspk.psl b/examples/nspk.psl similarity index 100% rename from examples/done_examples/nspk.psl rename to examples/nspk.psl diff --git a/examples/done_examples/wmf.psl b/examples/wmf.psl similarity index 100% rename from examples/done_examples/wmf.psl rename to examples/wmf.psl -- GitLab