...
 
Commits (2)
spec TESLA is
Theory
types Nat Zero One NonZero Bool True False .
subtypes NonZero Zero Key < Nat .
subtypes One < NonZero .
subtypes True False < Bool .
ops D N : -> NonZero .
ops T0 ZERO : -> Zero .
op ONE : -> One .
ops TS TR : -> Nat .
op TRUE : -> True .
op FALSE : -> False .
op _+_ : Nat Nat -> Nat [assoc comm id: ZERO] .
op _-_ : Nat Nat -> Nat .
op _*_ : Nat Nat -> Nat [assoc comm id: ONE] .
op leq : Nat Nat -> Bool [assoc] .
op equals : Nat Nat -> Bool [assoc comm] .
op geq : Nat Nat -> Bool [assoc] .
op Tfinal : Nat -> NonZero .
op TInit : Nat -> Nat .
var u : NonZero .
vars x y z : Nat .
var v : Nat .
vars tsrc trcv : Nat .
eq Tfinal(x) = +(T0,*(x,D)) .
eq TInit(u) = +(-(*(u,D),D)) .
eq TInit(ZERO) = T0 .
eq -(x,ZERO) = x .
eq equals(y,y) = TRUE .
eq equals(y,y) = TRUE .
eq equals(y,z) = FALSE .
eq leq(y,z) = equals(y,+(z,v)) .
eq geq(y,z) = leq(z,y) .
eq leq(ZERO,x) = TRUE .
eq leq(x,N) = TRUE .
eq leq(tsrc,+(trcv, -(TR,TS))) = TRUE .
This diff is collapsed.
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Diffie-Hellman.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
EOF
date
This source diff could not be displayed because it is too large. You can view the blob instead.
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Diffie-Hellman.maude
red genGrammars .
red run(1,0) .
red summary(1,1) .
red summary(1,2) .
red summary(1,3) .
red summary(1,4) .
red summary(1,5) .
red summary(1,6) .
red summary(1,7) .
red summary(1,8) .
red summary(1,9) .
red run(1,1) .
red run(1,2) .
red run(1,3) .
red run(1,4) .
red run(1,5) .
red run(1,6) .
red run(1,7) .
red run(1,8) .
red run(1,9) .
EOF
date
This source diff could not be displayed because it is too large. You can view the blob instead.
***(
The informal journal-level description of this protocol is as follows:
A --> B: A ; B ; exp(g,N_A)
B --> A: A ; B ; exp(g,N_A)
A --> B: enc(exp(exp(g,N_B),N_A),secret(A,B))
where N_A and N_B are nonces, exp(x,y) means x raised to y, enc(x,y) means
message y encripted using key x, and secret(A,B) is a secret shared between
A and B. Moreover, exponentiation and encription/decription have the following
algebraic properties:
exp(exp(X,Y),Z) = exp(X, Y * Z)
e(K,d(K,M)) = M .
d(K,e(K,M)) = M .
where * is the xor operator, though no algebraic property is given, since
they are not necessary for this protocol. However, note that the property
for exponentiation is restricted below by using appopriate sorts
in such a way that variable X can be only the generator g. This is necessary
to have a finitary unification procedure based on narrowing.
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Sort Information
sorts Name Nonce NeNonceSet Gen Exp Key GenvExp Secret .
subsort Gen Exp < GenvExp .
subsort Name NeNonceSet GenvExp Secret Key < Msg .
subsort Exp < Key .
subsort Name < Public . --- This is quite relevant and necessary
subsort Gen < Public . --- This is quite relevant and necessary
--- Secret
op sec : Name Fresh -> Secret [frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Intruder
ops a b i : -> Name .
--- Encryption
op e : Key Msg -> Msg [frozen] .
op d : Key Msg -> Msg [frozen] .
--- Exp
op exp : GenvExp NeNonceSet -> Exp [frozen] .
--- Gen
op g : -> Gen .
--- NeNonceSet
subsort Nonce < NeNonceSet .
op _*_ : NeNonceSet NeNonceSet -> NeNonceSet [frozen assoc comm] .
--- Concatenation
op _;_ : Msg Msg -> Msg [frozen gather (e E)] .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
eq exp(exp(W:Gen,Y:NeNonceSet),Z:NeNonceSet)
= exp(W:Gen, Y:NeNonceSet * Z:NeNonceSet) [variant] .
eq e(K:Key,d(K:Key,M:Msg)) = M:Msg [variant] .
eq d(K:Key,e(K:Key,M:Msg)) = M:Msg [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
vars NS1 NS2 NS3 NS : NeNonceSet .
var NA NB N : Nonce .
var GE : GenvExp .
var G : Gen .
vars A B : Name .
vars r r' r1 r2 r3 : Fresh .
var Ke : Key .
vars XE YE : Exp .
vars M M1 M2 : Msg .
var Sr : Secret .
eq STRANDS-DOLEVYAO =
:: nil :: [ nil | -(M1 ; M2), +(M1), nil ] &
:: nil :: [ nil | -(M1 ; M2), +(M2), nil ] &
:: nil :: [ nil | -(M1), -(M2), +(M1 ; M2), nil ] &
:: nil :: [ nil | -(Ke), -(M), +(e(Ke,M)), nil ] &
:: nil :: [ nil | -(Ke), -(M), +(d(Ke,M)), nil ] &
:: nil :: [ nil | -(NS1), -(NS2), +(NS1 * NS2), nil ] &
:: nil :: [ nil | -(GE), -(NS), +(exp(GE,NS)), nil ] &
:: r :: [ nil | +(n(i,r)), nil ] &
:: nil :: [ nil | +(g), nil ] &
:: nil :: [ nil | +(A), nil ]
[nonexec] .
eq STRANDS-PROTOCOL =
:: r,r' ::
[nil | +(A ; B ; exp(g,n(A,r))),
-(A ; B ; XE),
+(e(exp(XE,n(A,r)),sec(A,r'))), nil] &
:: r ::
[nil | -(A ; B ; XE),
+(A ; B ; exp(g,n(B,r))),
-(e(exp(XE,n(B,r)),Sr)), nil]
[nonexec] .
eq EXTRA-GRAMMARS
= (grl empty => (NS * n(a,r)) inL . ;
grl empty => n(a,r) inL . ;
grl empty => (NS * n(b,r)) inL . ;
grl empty => n(b,r) inL .
! S2 )
[nonexec] .
eq ATTACK-STATE(0)
= :: r ::
[nil, -(a ; b ; XE),
+(a ; b ; exp(g,n(b,r))),
-(e(exp(XE,n(b,r)),sec(a,r'))) | nil]
|| empty
|| nil
|| nil
|| never
*** Pattern for authentication
(:: R:FreshSet ::
[nil | +(a ; b ; XE),
-(a ; b ; exp(g,n(b,r))),
+(e(YE,sec(a,r'))), nil]
& S:StrandSet || K:IntruderKnowledge)
[nonexec] .
eq ATTACK-STATE(1)
= :: r ::
[nil, -(a ; b ; XE),
+(a ; b ; exp(g,n(b,r))),
-(e(exp(XE,n(b,r)),sec(a,r'))) | nil]
|| sec(a,r') inI
|| nil
|| nil
|| nil
[nonexec] .
eq ATTACK-STATE(2)
= :: r ::
[nil, -(a ; b ; XE),
+(a ; b ; exp(g,n(b,r))),
-(e(exp(XE,n(b,r)),sec(a,r'))) | nil]
|| sec(a,r') inI
|| nil
|| nil
|| never(
*** Avoid infinite useless path
(:: nil ::
[ nil | -(exp(GE,NS1 * NS2)), -(NS3),
+(exp(GE,NS1 * NS2 * NS3)), nil ]
& S:StrandSet || K:IntruderKnowledge)
*** Pattern to avoid unreachable states
(:: nil ::
[nil | -(exp(#1:Exp, N1:Nonce)),
-(sec(A:Name, #2:Fresh)),
+(e(exp(#1:Exp, N2:Nonce), sec(A:Name, #2:Fresh))), nil]
& S:StrandSet || K:IntruderKnowledge)
*** Pattern to avoid unreachable states
(:: nil ::
[nil | -(exp(#1:Exp, N1:Nonce)),
-(e(exp(#1:Exp, N1:Nonce), S:Secret)),
+(S:Secret), nil]
& S:StrandSet || K:IntruderKnowledge)
*** Pattern to avoid unreachable states
(S:StrandSet
|| (#4:Gen != #0:Gen), K:IntruderKnowledge)
)
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Needham_Schroeder.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red summary(10) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
red run(10) .
EOF
date
This diff is collapsed.
***(
The informal journal-level description of this protocol is as follows:
A --> B: pk(B,A ; N_A)
B --> A: pk(A, N_A ; N_B)
A --> B: pk(B, N_B)
where N_A and N_B are nonces, pk(x,y) means message y encripted using public
key x, and sk(x,y) means message y encripted using private key x.
Moreover, encription/decription have the following algebraic properties:
pk(K,sk(K,M)) = M .
sk(K,pk(K,M)) = M .
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Sort Information
sorts Name Nonce Key .
subsort Name Nonce Key < Msg .
subsort Name < Key .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Key Msg -> Msg [frozen] .
op sk : Key Msg -> Msg [frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Associativity operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
var Z : Msg .
var Ke : Key .
*** Encryption/Decryption Cancellation
eq pk(Ke,sk(Ke,Z)) = Z [variant] .
eq sk(Ke,pk(Ke,Z)) = Z [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
var Ke : Key .
vars X Y Z : Msg .
vars r r' : Fresh .
vars A B : Name .
vars N N1 N2 : Nonce .
eq STRANDS-DOLEVYAO
= :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(Ke,X)), nil ] &
:: nil :: [ nil | +(A), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r ::
[ nil | +(pk(B,A ; n(A,r))), -(pk(A,n(A,r) ; N)), +(pk(B, N)), nil ] &
:: r ::
[ nil | -(pk(B,A ; N)), +(pk(A, N ; n(B,r))), -(pk(B,n(B,r))), nil ]
[nonexec] .
eq ATTACK-STATE(0)
= :: r ::
[ nil, -(pk(b,a ; N)), +(pk(a, N ; n(b,r))), -(pk(b,n(b,r))) | nil ]
|| n(b,r) inI, empty
|| nil
|| nil
|| nil
[nonexec] .
eq ATTACK-STATE(1)
= :: r ::
[ nil, -(pk(b,a ; N)), +(pk(a, N ; n(b,r))), -(pk(b,n(b,r))) | nil ]
|| empty
|| nil
|| nil
|| never *** for authentication
(:: r' ::
[ nil, +(pk(b,a ; N)), -(pk(a, N ; n(b,r))) | +(pk(b,n(b,r))), nil ]
& S:StrandSet
|| K:IntruderKnowledge)
[nonexec] .
eq ATTACK-STATE(2)
= :: r ::
[ nil, +(pk(b,a ; n(a,r))), -(pk(a,n(a,r) ; N1)), +(pk(b, N1)) | nil ] &
:: r' ::
[ nil, -(pk(b,a ; N2)), +(pk(a, N2 ; n(b,r'))), -(pk(b,n(b,r'))) | nil ]
|| N2 != n(a,r)
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Needham_Schroeder_Lowe.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
EOF
date
This diff is collapsed.
--- Nedhham-Schroeder-Lowe Modified Protocol
***(
The informal journal-level description of this protocol is as follows:
A --> B: pk(B,A ; N_A)
B --> A: pk(A, N_A ; N_B ; B)
A --> B: pk(B, N_B)
where N_A and N_B are nonces, pk(x,y) means message y encripted using public
key x, and sk(x,y) means message y encripted using private key x.
Moreover, encription/decription have the following algebraic properties:
pk(K,sk(K,M)) = M .
sk(K,pk(K,M)) = M .
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Sort Information
sorts Name Nonce Key .
subsort Name Nonce Key < Msg .
subsort Name < Key .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Key Msg -> Msg [frozen] .
op sk : Key Msg -> Msg [frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Associativity operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
var Z : Msg .
var Ke : Key .
*** Encryption/Decryption Cancellation
eq pk(Ke,sk(Ke,Z)) = Z [variant] .
eq sk(Ke,pk(Ke,Z)) = Z [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
var Ke : Key .
vars X Y Z : Msg .
vars r r' : Fresh .
vars A B : Name .
vars N N1 N2 : Nonce .
eq STRANDS-DOLEVYAO
= :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(Ke,X)), nil ] &
:: nil :: [ nil | +(A), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r ::
[ nil | +(pk(B,A ; n(A,r))), -(pk(A,n(A,r) ; N ; B)), +(pk(B, N)), nil ] &
:: r ::
[ nil | -(pk(B,A ; N)), +(pk(A, N ; n(B,r) ; B)), -(pk(B,n(B,r))), nil ]
[nonexec] .
eq ATTACK-STATE(0)
= :: r ::
[ nil, -(pk(b,a ; N)), +(pk(a, N ; n(b,r) ; b)), -(pk(b,n(b,r))) | nil ]
|| n(b,r) inI, empty
|| nil
|| nil
|| nil
[nonexec] .
eq ATTACK-STATE(1) --- authentication
= :: r ::
[ nil, -(pk(b,a ; N)), +(pk(a, N ; n(b,r) ; b)), -(pk(b,n(b,r))) | nil ]
|| empty
|| nil
|| nil
|| never(
(:: r' ::
[ nil | +(pk(b,a ; N1)), -(pk(a,N1 ; n(b,r) ; b)), +(pk(b, n(b,r))), nil ]
& SS:StrandSet)
|| IK:IntruderKnowledge
)
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Needham_Schroeder_Lowe_ECB.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red summary(10) .
red summary(11) .
red summary(12) .
red summary(13) .
red summary(14) .
red summary(15) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
red run(10) .
red run(11) .
red run(12) .
red run(13) .
red run(14) .
red run(15) .
EOF
date
This diff is collapsed.
***(
The informal journal-level description of this protocol is as follows:
1. A -> B : {Na, A}PK(B)
2. B -> A : {Na, Nb, B}PK(A)
3. A -> B : {Nb}PK(B)
where PK is homomorphic over concatenation.
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Sort Information
sorts Name Nonce Key .
subsort Name Nonce Key < Msg .
subsort Name < Key .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Msg Key -> Msg [frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Associativity operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
eq pk(X:Msg ; Y:Msg, K:Key) = pk(X:Msg, K:Key) ; pk(Y:Msg, K:Key)
[nonexec label homomorphism metadata "builtin-unify"] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
var Ke : Key .
vars X Y Z : Msg .
vars r r' : Fresh .
vars A B : Name .
vars N NA NB : Nonce .
eq STRANDS-DOLEVYAO
= :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(pk(X,Ke)), nil ] &
:: nil :: [ nil | -(pk(X,i)), +(X), nil ] &
:: nil :: [ nil | +(A), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r ::
[ nil | +(pk(A ; n(A,r), B)), -(pk(n(A,r) ; NB ; B, A)), +(pk(NB, B)), nil ] &
:: r ::
[ nil | -(pk(A ; NA, B)), +(pk(NA ; n(B,r) ; B, A)), -(pk(n(B,r), B)), nil ]
[nonexec] .
eq ATTACK-STATE(0)
= :: r ::
[ nil, -(pk(a ; NA, b)), +(pk(NA ; n(b,r) ; b,a)), -(pk(n(b,r), b)) | nil ]
|| n(b,r) inI, empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Needham_Schroeder_Lowe_XOR.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red summary(10) .
red summary(11) .
red summary(12) .
red summary(13) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
red run(10) .
red run(11) .
red run(12) .
red run(13) .
EOF
date
This diff is collapsed.
***(
Lowe's fix but with an attack using exlusive or.
The informal journal-level description [Hosc07] of this protocol is as follows:
A --> B: pk(B, N_A ; A)
B --> A: pk(A, N_A ; B * N_B)
A --> B: pk(B, N_B)
where N_A and N_B are nonces, pk(x,y) means message y encripted using public
key x, and sk(x,y) means message y encripted using private key x.
Symbol * is the exclusive or operator.
Encription/decription have the following algebraic properties:
pk(K,sk(K,M)) = M .
sk(K,pk(K,M)) = M .
And exclusive or has the following algebraic properties:
X * X = 0 .
X * X * Y = Y .
X * 0 = X .
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Sort Information
sorts Name Nonce NNSet .
subsort Name Nonce NNSet < Msg .
subsort Name < Public .
subsort Name Nonce < NNSet .
--- Encoding operators for public/private encryption
op pk : Name Msg -> Msg [frozen] .
op sk : Name Msg -> Msg [frozen] .
--- Concatenation operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Exclusive or
op _*_ : NNSet NNSet -> NNSet [assoc comm frozen] .
op null : -> NNSet .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
var A : Name .
vars X Y Z : Msg .
vars XN YN : NNSet .
*** Encryption/Decryption Cancellation
eq pk(A,sk(A,Z)) = Z [variant] .
eq sk(A,pk(A,Z)) = Z [variant] .
*** Exclusive or properties
eq XN * XN = null [variant] .
eq XN * XN * YN = YN [variant] .
eq XN * null = XN [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
vars X Y Z : Msg .
vars r r' : Fresh .
vars A B : Name .
vars N NA NB : Nonce .
vars XN YN : NNSet .
eq STRANDS-DOLEVYAO
= :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(XN), -(YN), +(XN * YN), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(A,X)), nil ] &
:: nil :: [ nil | +(null), nil ] &
:: r :: [ nil | +(n(i,r)), nil ] &
:: nil :: [ nil | +(A), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r :: *** Bob ***
[nil | +(pk(B, n(A,r) ; A)),
-(pk(A, n(A,r) ; B * YN)),
+(pk(B, YN)), nil]
&
:: r' :: *** Alice ***
[nil | -(pk(B, XN ; A)),
+(pk(A, XN ; B * n(B,r'))),
-(pk(B,n(B,r'))), nil]
[nonexec] .
eq ATTACK-STATE(0)
= :: r' :: *** Alice ***
[nil, -(pk(b, XN ; a)),
+(pk(a, XN ; b * n(b,r'))),
-(pk(b, n(b,r'))) | nil]
|| n(b,r') inI, empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/Needham_Schroeder_Lowe_assoc.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red initials(5) .
EOF
date
This diff is collapsed.
--- Nedhham-Schroeder-Lowe Modified Protocol
***(
The informal journal-level description of this protocol is as follows:
A --> B: pk(B,A ; N_A)
B --> A: pk(A, N_A ; N_B ; B)
A --> B: pk(B, N_B)
where N_A and N_B are nonces, pk(x,y) means message y encripted using public
key x, and sk(x,y) means message y encripted using private key x.
Moreover, encription/decription have the following algebraic properties:
pk(K,sk(K,M)) = M .
sk(K,pk(K,M)) = M .
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Sort Information
sorts Name Nonce Key .
subsort Name Nonce Key < Msg .
subsort Name < Key .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Key Msg -> Msg [frozen] .
op sk : Key Msg -> Msg [frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Associativity operator
op _;_ : Msg Msg -> Msg [assoc frozen] .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
var Z : Msg .
var Ke : Key .
*** Encryption/Decryption Cancellation
eq pk(Ke,sk(Ke,Z)) = Z [variant] .
eq sk(Ke,pk(Ke,Z)) = Z [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
var Ke : Key .
vars X Y Z : Msg .
vars r r' : Fresh .
vars A B : Name .
vars NA NB : Msg .
eq STRANDS-DOLEVYAO
= :: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(Ke,X)), nil ] &
:: nil :: [ nil | +(A), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r ::
[ nil | +(pk(B,A ; n(A,r))), -(pk(A,n(A,r) ; NB ; B)), +(pk(B, NB)), nil ] &
:: r ::
[ nil | -(pk(B,A ; NA)), +(pk(A, NA ; n(B,r) ; B)), -(pk(B,n(B,r))), nil ]
[nonexec] .
eq ATTACK-STATE(0)
= :: r ::
[ nil, -(pk(b,a ; NA)), +(pk(a, NA ; n(b,r) ; b)), -(pk(b,n(b,r))) | nil ]
|| n(b,r) inI, empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
***(
NonDet Choice between public key encryption (denoted by pubKey)
1. A -> B: A, B, pubKey
2. B -> A: (B, SK)_pk(A)
3. A -> B: (A , SK, N_A)_pk(B)
4. B -> A: (B, N_A)_pk(A)
and shared key encryption (denoted by sharedKey)
1. A -> B: A, B, sharedKey
2. B -> A: (B, SK)_key(A,B)
3. A -> B: (A , SK, N_A)_key(A,B)
4. B -> A : (B, N_A)_key(A,B)
)***
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
sort Name Nonce SKey Key Mode .
subsort Name Nonce SKey Key Mode < Msg .
subsort Name < Public .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Modes
ops pubkey shkey : -> Mode .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Concatenation operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
--- Key
op key : Name Name -> Key [frozen] .
--- Session Key
op skey : Name Fresh -> SKey [frozen] .
--- Public encryption
op pk : Name Msg -> Msg [frozen] .
op sk : Name Msg -> Msg [frozen] .
--- Shared key encryption
op she : Key Msg -> Msg [frozen] .
op shd : Key Msg -> Msg [frozen] .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
--- Variables
vars X Y Z : Msg .
vars A B : Name .
var Ke : Key .
eq pk(A, sk(A, Z)) = Z [variant] .
eq sk(A, pk(A, Z)) = Z [variant] .
eq she(Ke, shd(Ke, Z)) = Z [variant] .
eq shd(Ke, she(Ke, Z)) = Z [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
vars X Y : Msg .
var r r' : Fresh .
var A B : Name .
var N NA NB NA' NB' : Nonce .
var Ke : Key .
var SK : SKey .
var mode : Mode .
eq STRANDS-DOLEVYAO
=
:: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(pk(A, X)), nil ] &
:: nil :: [ nil | -(X), +(sk(i, X)), nil ] &
:: nil :: [ nil | -(Ke), -(X), +(she(Ke, X)), nil ] &
:: nil :: [ nil | -(Ke), -(X), +(shd(Ke, X)), nil ] &
:: nil :: [ nil | +(key(i, A)), nil ] &
:: nil :: [ nil | +(key(A, i)), nil ] &
:: r :: [ nil | +(skey(i,r)), nil ] &
:: r :: [ nil | +(n(i,r)), nil ] &
:: nil :: [ nil | +(A) , nil ]
[nonexec] .
eq PROCESSES-PROTOCOL
= (
( +(A ; B ; pubkey) .
-(pk(A, B ; SK)) .
+(pk(B, A ; SK ; n(A,r))) .
-(pk(A, B ; n(A,r)))
)
?
( +(A ; B ; shkey) .
-(she(key(A, B), SK )) .
+(she(key(A, B), SK ; n(A,r))) .
-(she(key(A,B), n(A,r))) )
)
&
( -(A ; B ; mode) .
(if (mode eq pubkey)
then ( +(pk(A, B ; skey(B, r))) .
-(pk(B, A ; skey(B,r) ; N)) .
+(pk(A, B ; N)) )
else ( +(she(key(A, B), skey(B,r))) .
-(she(key(A, B), skey(B,r) ; N)) .
+(she(key(A,B), N)) )
)
)
[nonexec] .
--- regular execution with shared key encryption
eq ATTACK-PROCESS(0)
= +(a ; b ; shkey) .
-(she(key(a, b), SK )) .
+(she(key(a, b), SK ; n(a,r))) .
-(she(key(a, b), n(a,r)))
|| empty
|| nil
[nonexec] .
--- regular execution with public key encryption
eq ATTACK-PROCESS(1)
= +(a ; b ; pubkey) .
-(pk(a, b ; SK)) .
+(pk(b, a ; SK ; n(a,r))) .
-(pk(a, b ; n(a,r)))
|| empty
|| nil
[nonexec] .
--- intruder learns the session key
eq ATTACK-PROCESS(2)
= -(a ; b ; mode) .
(mode neq pubkey) .
+(she(key(a, b), skey(b,r))) .
-(she(key(a, b), skey(b,r) ; N)) .
+(she(key(a, b), N))
|| skey(b,r) inI
|| nil
[nonexec] .
--- intruder learns the session key
eq ATTACK-PROCESS(3)
= -(a ; b ; mode) .
(mode eq pubkey) .
+(pk(a, b ; skey(b, r))) .
-(pk(b, a ; skey(b,r) ; N)) .
+(pk(a, b ; N))
|| skey(b,r) inI
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
\ No newline at end of file
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/nsl-db-dc.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red summary(10) .
red summary(11) .
red summary(12) .
red summary(13) .
red summary(14) .
red summary(15) .
red summary(16) .
red summary(17) .
red summary(18) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
red run(10) .
red run(11) .
red run(12) .
red run(13) .
red run(14) .
red run(15) .
red run(16) .
red run(17) .
red run(18) .
EOF
date
This diff is collapsed.
--- Direct Composition
--- NSL-Distance Bounding protocol
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Synchronization for composition
subsort Role < Msg .
--- Roles
ops init-nsl resp-nsl : -> Role .
ops init-db resp-db : -> Role .
--- Sort Information
sorts Name Nonce NonceSet .
subsort Name NonceSet < Msg .
subsort Nonce < NonceSet .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Name Msg -> Msg [frozen] .
op sk : Name Msg -> Msg [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Concatenation operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
--- Exclusive-or operator
op _*_ : NonceSet NonceSet -> NonceSet [assoc comm frozen] .
op null : -> NonceSet .
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
--- Variables
vars X Y Z : Msg .
vars A B : Name .
vars XN YN : NonceSet .
*** Encryption/Decryption Cancellation
eq pk(A,sk(A,Z)) = Z [variant] .
eq sk(A,pk(A,Z)) = Z [variant] .
*** Exclusive or properties
eq null * XN = XN [variant] .
eq XN * XN = null [variant] .
eq XN * XN * YN = YN [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
vars r r' r'' r# : Fresh .
vars A B C : Name .
vars NA NB N N' NC : Nonce .
vars NS NS' : NonceSet .
vars X Y Z H : Msg .
vars P Q : Name .
eq STRANDS-DOLEVYAO
=
--- :: nil :: [ nil | -(NS), -(NS'), +(NS * NS'), nil ] &
:: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(A,X)), nil ] &
:: nil :: [ nil | +(A) , nil ] &
:: nil :: [ nil | +(null), nil ] &
:: r :: [ nil | +(n(i,r)), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
= :: r :: --- NSL-Alice
[ nil | +(pk(B, n(A,r) ; A)) ,
-(pk(A, n(A,r) ; NB ; B )),
+(pk(B, NB)),
{init-nsl -> resp-db ;; 1-1 ;; A ; B ; n(A,r)}, nil ] &
:: r :: --- NSL-Bob
[ nil | -(pk(B,NA ; A)),
+(pk(A, NA ; n(B,r) ; B)),
-(pk(B,n(B,r))),
{resp-nsl -> init-db ;; 1-1 ;; A ; B ; NA}, nil ] &
:: r' ::
[ nil | {resp-nsl -> init-db ;; 1-1 ;; A ; B ; NA},
+(n(B,r')),
-(NA * n(B,r')), nil] &
:: nil ::
[ nil | {init-nsl -> resp-db ;; 1-1 ;; A ; B ; NA },
-(N),
+(NA * N), nil ]
[nonexec] .
--- Attack pattern to find Distance Hijacking attack
eq ATTACK-STATE(0)
= :: r ::
[ nil, +(pk(i,n(a,r) ; a)),
-(pk(a,n(a,r) ; NC ; i)),
+(pk(i, NC)),
{init-nsl -> resp-db ;; 1-1 ;; a ; i ; n(a,r) } | nil] &
:: r'' ::
[ nil, {resp-nsl -> init-db ;; 1-1 ;; i ; b ; n(a,r)},
+(n(b,r'')),
-(n(a,r) * n(b,r'')) | nil]
|| empty
|| nil
|| nil
|| nil
[nonexec] .
--- Attack pattern to find Distance Hijacking attack
eq ATTACK-STATE(1)
= :: r ::
[ nil, +(pk(i,n(a,r) ; a)),
-(pk(a,n(a,r) ; NC ; i)),
+(pk(i, NC)),
{init-nsl -> resp-db ;; 1-1 ;; a ; i ; n(a,r) } | nil] &
:: r' ::
[ nil, -(pk(b,n(a,r) ; i)),
+(pk(i,n(a,r) ; n(b,r') ; b)),
-(pk(b,n(b,r'))),
{resp-nsl -> init-db ;; 1-1 ;; i ; b ; n(a,r) } | nil ] &
:: r'' ::
[ nil, {resp-nsl -> init-db ;; 1-1 ;; i ; b ; n(a,r)},
+(n(b,r'')),
-(n(a,r) * n(b,r'')) | nil] &
:: nil ::
[ nil, {init-nsl -> resp-db ;; 1-1 ;; a ; i ; n(a,r) },
-(n(b,r'')),
+(n(a,r) * n(b,r'')) | nil ]
|| empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/nsl-kd-dc.maude
red genGrammars .
red run(0) .
red summary(1) .
red summary(2) .
red summary(3) .
red summary(4) .
red summary(5) .
red summary(6) .
red summary(7) .
red summary(8) .
red summary(9) .
red summary(10) .
red summary(11) .
red summary(12) .
red summary(13) .
red summary(14) .
red summary(15) .
red summary(16) .
red summary(17) .
red summary(18) .
red summary(19) .
red summary(20) .
red summary(21) .
red summary(22) .
red summary(23) .
red summary(24) .
red run(1) .
red run(2) .
red run(3) .
red run(4) .
red run(5) .
red run(6) .
red run(7) .
red run(8) .
red run(9) .
red run(10) .
red run(11) .
red run(12) .
red run(13) .
red run(14) .
red run(15) .
red run(16) .
red run(17) .
red run(18) .
red run(19) .
red run(20) .
red run(21) .
red run(22) .
red run(23) .
red run(24) .
EOF
date
This diff is collapsed.
--- Direct composition
--- NSL-Key Distribution protocol composition
fmod PROTOCOL-EXAMPLE-SYMBOLS is
--- Importing sorts Msg, Fresh, Public, and GhostData
protecting DEFINITION-PROTOCOL-RULES .
----------------------------------------------------------
--- Overwrite this module with the syntax of your protocol
--- Notes:
--- * Sort Msg and Fresh are special and imported
--- * Every sort must be a subsort of Msg
--- * No sort can be a supersort of Msg
----------------------------------------------------------
--- Synchronization for composition
subsort Role < Msg .
--- Roles
ops init-nsl resp-nsl : -> Role .
ops init-kd resp-kd : -> Role .
--- Sort Information
sorts Name Nonce MKey SKey .
subsort Name Nonce MKey SKey < Msg .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Name Msg -> Msg [frozen] .
op sk : Name Msg -> Msg [frozen] .
--- Nonce operator
op n : Name Fresh -> Nonce [frozen] .
--- Concatenation operator
op _;_ : Msg Msg -> Msg [gather (e E) frozen] .
--- Hash operator
op h : Nonce Nonce -> MKey [ frozen ] .
--- Key operator
op skey : Name Fresh -> SKey [ frozen ] .
--- Encryption Operators
op e : MKey Msg -> Msg [frozen] .
op d : MKey Msg -> Msg [frozen] .
--- Principals
op a : -> Name . --- Alice
op b : -> Name . --- Bob
op i : -> Name . --- Intruder
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
----------------------------------------------------------
--- Overwrite this module with the algebraic properties
--- of your protocol
----------------------------------------------------------
--- Variables
vars Z : Msg .
var A : Name .
vars MKe : MKey .
*** Encryption/Decryption Cancellation
eq pk(A,sk(A,Z)) = Z [variant] .
eq sk(A,pk(A,Z)) = Z [variant] .
eq d(MKe,e(MKe,Z)) = Z [variant] .
eq e(MKe,d(MKe,Z)) = Z [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
----------------------------------------------------------
--- Overwrite this module with the strands
--- of your protocol
----------------------------------------------------------
vars r r' : Fresh .
vars A B C D : Name .
vars NA NB N : Nonce .
vars X Y : Msg .
var MKe : MKey .
var K KA KB : SKey .
var rK : Role .
vars NA' NB' : Nonce .
eq STRANDS-DOLEVYAO
=
:: nil :: [ nil | -(X), -(Y), +(X ; Y), nil ] &
:: nil :: [ nil | -(X ; Y), +(X), nil ] &
:: nil :: [ nil | -(X ; Y), +(Y), nil ] &
:: nil :: [ nil | -(X), +(sk(i,X)), nil ] &
:: nil :: [ nil | -(X), +(pk(A,X)), nil ] &
:: nil :: [ nil | +(A) , nil ] &
:: r :: [ nil | +(n(i,r)), nil ] &
:: nil :: [ nil | -(MKe), -(X), +(e(MKe,X)), nil ] &
:: nil :: [ nil | -(MKe), -(X), +(d(MKe,X)), nil ] &
:: r :: [ nil | -(N), +(h(n(i,r), N)), nil ] &
:: r :: [ nil | -(N), +(h(N, n(i,r))), nil ] &
:: r :: [ nil | +(skey(i,r)), nil ]
[nonexec] .
eq STRANDS-PROTOCOL
=
--- NSL protocol
:: r ::
[ nil | +(pk(B, n(A,r) ; A)) ,
-(pk(A, n(A,r) ; NB ; B )),
+(pk(B, NB)),
{ init-nsl -> init-kd resp-kd ;; 1-* ;; A ; B ; h(n(A,r) , NB) }, nil ] &
:: r ::
[ nil | -(pk(B,NA ; A)),
+(pk(A, NA ; n(B,r) ; B)),
-(pk(B,n(B,r))),
{resp-nsl -> init-kd resp-kd ;; 1-* ;; B ; A ; h(NA , n(B,r))}, nil ] &
---- KD protocol
:: r' ::
[ nil | { init-nsl resp-nsl -> init-kd ;; 1-* ;; C ; D ; MKe },
+(e(MKe, skey(C, r'))) ,
-(e(MKe, skey(C, r') ; N)),
+(e(MKe, N)), nil] &
:: r' ::
[ nil | { init-nsl resp-nsl -> resp-kd ;; 1-* ;; C ; D ; MKe },
-(e(MKe, K)),
+(e(MKe, K ; n(C,r'))),
-(e(MKe, n(C,r'))), nil ]
[nonexec] .
--- Attack pattern to find secrecy attack
eq ATTACK-STATE(0)
= :: r' ::
[ nil, { init-nsl -> init-kd ;; 1-* ;; a ; b ; MKe },
+(e(MKe, skey(a, r'))) ,
-(e(MKe, skey(a, r') ; n(b,r))),
+(e(MKe, n(b,r))) | nil] &
:: r ::
[ nil, { resp-nsl -> resp-kd ;; 1-* ;; a ; b ; MKe },
-(e(MKe, skey(a,r'))),
+(e(MKe, skey(a,r') ; n(b,r))),
-(e(MKe, n(b,r))) | nil ]
|| skey(a, r') inI
|| nil
|| nil
|| nil
[nonexec] .
--- Attack pattern to find regular execution of the protocol
eq ATTACK-STATE(1)
= :: r' ::
[ nil, { init-nsl -> init-kd ;; 1-* ;; a ; b ; MKe },
+(e(MKe, skey(a, r'))) ,
-(e(MKe, skey(a, r') ; n(b,r))),
+(e(MKe, n(b,r))) | nil] &
:: r ::
[ nil, { resp-nsl -> resp-kd ;; 1-* ;; a ; b ; MKe },
-(e(MKe, skey(a,r'))),
+(e(MKe, skey(a,r') ; n(b,r))),
-(e(MKe, n(b,r))) | nil ]
|| empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/rock-paper-scissors.maude
red genGrammars .
red summary(0,0) .
red summary(0,1) .
red summary(0,2) .
red summary(0,3) .
red summary(0,4) .
red summary(0,5) .
red summary(0,6) .
red initials(0,6) .
EOF
date
This diff is collapsed.
date
#!/bin/bash
maude271 <<EOF
load maude-npa.maude
load examples/rock-paper-scissors.maude
red genGrammars .
red summary(1,0) .
red summary(1,1) .
EOF
date
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7.1 built: Jun 27 2016 16:43:23
Copyright 1997-2016 SRI International
Thu Aug 10 12:49:04 2017
Maude>
Maude-NPA Version: July 30th 2017
with direct composition and irreducibility constraints
(To be run with Maude 2.7.1 or above)
Copyright (c) 2017, University of Illinois
All rights reserved.
Commands:
red unification? . returns the unification algorithm to be used
red new-strands? . returns the actual protocol strands
red displayGrammars . for generating grammars
red run(X,Y). for Y backwards analysis steps for attack pattern X
red debug(X,Y). more information than run command
red digest(X,Y). less information than run command
red summary(X,Y). for summary of analysis steps
red ids(X,Y). for set of state ids
red initials(X,Y). for showing only initial steps