Skip to content

GitLab

V
VerifyTESLA
Commit 2e7f49d9 authored by acholewa's avatar acholewa
Browse files
Options

Removed composition_examples from the main branch. Also tweaked some of the comments in psl.maude

parent 13c634dc
Hide whitespace changes
Inline Side-by-side
Showing with 3 additions and 872 deletions
composition_examples/debugging_maude/comp_nsl_db.maude deleted 100644 → 0
View file @ 13c634dc
load psl.maude
select COMP-TRANSLATION-TO-MAUDE-NPA .
rew [comp(1, 2) |->
nsl-A ;1 db-B : A |-> B, B |-> A, NO |-> n(A, r:Fresh) .[3]
nsl-B ;1 db-A : B |-> A1, A |-> B, NO |-> NA1 .[3]
]
[mt]
---Only here for purposes of debugging.
---Note: This should be added by Python if there are no attacks.
[$emptyAttackData]
translate(1,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(nsl-A) = A, B .[1]
In(nsl-B) = B .[1]
1 . nsl-A -> nsl-B : pk(B, n(A, r:Fresh) ; A) |-
pk(B, NA1 ; A1) .[1]
2 . nsl-B -> nsl-A : pk(A1, NA1 ; n(B, r1:Fresh) ; B) |-
pk(A , n(A, r:Fresh) ; NB ; B) .[1]
3 . nsl-A -> nsl-B : pk(B, NB) |-
pk(B, n(B, r1:Fresh)) .[1]
Out(nsl-A) = A, B, n(A, r:Fresh), NB, h(n(A, r:Fresh) ; NB) .[1]
Out(nsl-B) = A1, B, NA1, n(B, r1:Fresh), h(NA1 ; n(B, r1:Fresh)) .[1]
}
Intruder
{
=> C .[1]
X, Y <=> X ; Y .[1]
X => sk(i, X) .[1]
K, X => pk(K, X) .[1]
}
Attacks
{
0 .
{
nsl-B executes protocol .[1]
Intruder learns n(B, r1:Fresh) .[1]
Subst(nsl-B) = B |-> b, A1 |-> a .[1]
}
}
}
)
translate(2,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(db-A) = A, B, NO .[2]
In(db-B) = A, B, NO .[2]
1 . db-A -> db-B : n(A, r:Fresh) |- NA .[2]
2 . db-B -> db-A : NO * NA |- NO * n(A, r:Fresh) .[2]
Out(db-A) = n(A, r:Fresh), NO * n(A, r:Fresh) .[2]
Out(db-B) = NA, NO * NA .[2]
}
Intruder
{
=> C, n(i, r:Fresh) .[2]
X, Y => X * Y .[2]
}
Attacks
{
0 .
{
db-B executes protocol .[2]
Subst(db-B) = A |-> a, B |-> b .[2]
}
}
}
) .
composition_examples/debugging_maude/comp_nsl_kd.maude deleted 100644 → 0
View file @ 13c634dc
---Only for debugging.
load psl.maude
select COMP-TRANSLATION-TO-MAUDE-NPA .
set print attribute off .
rew
[comp(1, 2) |->
nsl-A ;* kd-B : A |-> B, B |-> A, K |-> h(n(A, r) ; NB) .[3]
nsl-B ;* kd-A : A |-> B, B |-> A1, K |-> h(NA1 ; n(B, r1)) .[3]
nsl-A ;* kd-A : A |-> A, B |-> B, K |-> h(n(A, r) ; NB) .[3]
nsl-B ;* kd-B : A |-> A1, B |-> B, K |-> h(NA1 ; n(B, r1)) .[3]
]
[mt]
---Only here for purposes of debugging.
---Note: This should be added by Python if there are no attacks.
[$emptyAttackData]
translate(1,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(nsl-A) = A, B .[1]
In(nsl-B) = B .[1]
1 . nsl-A -> nsl-B : pk(B, n(A, r:Fresh) ; A) |-
pk(B, NA1 ; A1) .[1]
2 . nsl-B -> nsl-A : pk(A1, NA1 ; n(B, r1:Fresh) ; B) |-
pk(A , n(A, r:Fresh) ; NB ; B) .[1]
3 . nsl-A -> nsl-B : pk(B, NB) |-
pk(B, n(B, r1:Fresh)) .[1]
Out(nsl-A) = A, B, n(A, r:Fresh), NB, h(n(A, r:Fresh) ; NB) .[1]
Out(nsl-B) = A1, B, NA1, n(B, r1:Fresh), h(NA1 ; n(B, r1:Fresh)) .[1]
}
Intruder
{
=> C .[1]
X, Y <=> X ; Y .[1]
X => sk(i, X) .[1]
K, X => pk(K, X) .[1]
}
Attacks
{
0 .
{
nsl-B executes protocol .[1]
Intruder learns n(B, r1:Fresh) .[1]
Subst(nsl-B) = B |-> b, A1 |-> a .[1]
}
}
}
)
translate(2,
[$noDefs]
[mt]
[empty]
Specification
{
Protocol
{
In(kd-A) = A, B, K .[2]
In(kd-B) = A, B, K .[2]
1 . kd-A -> kd-B : e(K, skey(A, r)) |-
e(K, SK) .[2]
2 . kd-B -> kd-A : e(K, SK ; n(B, r1)) |-
e(K, skey(A, r) ; NB) .[2]
3 . kd-A -> kd-B : e(K, NB) |-
e(K, n(B, r1)) .[2]
Out(kd-A) = K, skey(A, r), NB .[2]
Out(kd-B) = A, B, K, SK, n(B, r1) .[2]
}
Intruder
{
=> C, n(i, r), skey(i, r) .[2]
K, X => e(K, X), d(K, X) .[2]
X, Y <=> X ; Y .[2]
}
Attacks
{
0 .
{
kd-B executes protocol .[2]
Subst(kd-B) = A |-> a, B |-> b .[2]
}
}
}
) .
q
Specification{
Protocol{
In(kd-A)= K,A,B .[2] .
In(kd-B)= K,A,B .[2]
1 . kd-A -> kd-B : e(K,skey(A, r)) |- e(K,SK) .[2] .
q
2 . kd-B -> kd-A : e(K,SK ; n(B, r1)) |- e(K,skey(A, r) ; NB) .[2]
3 . kd-A -> kd-B : e(K,NB) |- e(K,n(B, r1)) .[2]
Out(kd-A)= K,NB,skey(A, r) .[2]
Out(kd-B)= K,SK,A,B,n(B, r1) .[2]
}
Intruder{
emptyMsgSet => C .[2]
emptyMsgSet => skey(i, r) .[2]
emptyMsgSet => n(i, r) .[2]
K,X => e(K,X),d(K,X) .[2]
X,Y => X ; Y .[2]
X ; Y => X .[2]
X ; Y => Y .[2]
}
Attacks{
0 .{kd-B executes protocol .[2] Subst(kd-B)= A |-> a,B |-> b .[
2]}
}}
.
composition_examples/debugging_maude/nsl-db-dc.maude deleted 100644 → 0
View file @ 13c634dc
--- 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 Enc .
subsort Name NonceSet Enc < Msg .
subsort Nonce < NonceSet .
subsort Name < Public .
--- Encoding operators for public/private encryption
op pk : Name Msg -> Enc [frozen] .
op sk : Name Msg -> Enc [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' : 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 ] &
:: 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] .
var NC : Nonce .
--- Attack pattern to find Distance Hijacking attack
eq ATTACK-STATE(0)
= :: r ::
[ nil , +(pk(C,n(a,r) ; a)),
-(pk(a, n(a,r) ; NC ; C )),
+(pk(C, NC)) |
{init-nsl -> resp-db ;; 1-1 ;; a ; C ; n(a,r)},
nil] &
:: r' ::
[ nil, {resp-nsl -> init-db ;; 1-1 ;; P ; b ; n(a,r)},
+(n(b,r')), -(n(a,r) * n(b,r')) | nil]
|| (a != P) , (C != b )
|| nil
|| nil
|| nil
[nonexec] .
--- Attack pattern to find Simpler attack
eq ATTACK-STATE(1)
= :: r ::
[ nil , +(pk(C,n(a,r) ; a)) |
-(pk(a, n(a,r) ; NC ; C )),
+(pk(C, NC)),
{init-nsl -> resp-db ;; 1-1 ;; a ; C ; n(a,r)},
nil] &
:: r' ::
[ nil, {resp-nsl -> init-db ;; 1-1 ;; P ; b ; n(a,r)},
+(n(b,r')), -(n(a,r) * n(b,r')) | nil]
|| (a != P) , (C != b )
|| nil
|| nil
|| nil
[nonexec] .
endfm
--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .
composition_examples/debugging_maude/nsldb.maude deleted 100644 → 0
View file @ 13c634dc
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . --- -1
sorts Name Nonce Key .
subsort Name < Key .
subsort Name < Public .
subsorts Name Nonce Key < Msg .
ops pk sk : Key Msg -> Msg .
op n : Name Fresh -> Nonce .
ops a b i : -> Name . --- Alice Bob Intruder
op _;_ : Msg Msg -> Msg [gather (e E)] .
op h : Msg -> Key .
op _*_ : Msg Msg -> Msg [assoc comm] .
op 0 : -> Msg .
---------------Automatically generated and added by Python------------
ops nsl-A nsl-B : -> Role .
ops db-A db-B : -> Role .
---Used for building the message for the synchronization message.
op _$;_ : Msg Msg -> Msg [gather(E e)] .
----------End Automatically generated and added by Python-------------------
endfm
composition_examples/debugging_maude/nsldb_npa.maude deleted 100644 → 0
View file @ 13c634dc
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . --- -1
sorts Name Nonce Key .
subsort Name < Key .
subsort Name < Public .
ops pk sk : Key Msg -> Msg [frozen] .
op n : Name Fresh -> Nonce [frozen] .
ops a b i : -> Name . --- Alice Bob Intruder
op _;_ : Msg Msg -> Msg [frozen gather (e E)] .
op h : Msg -> Key [frozen] .
var Z : Msg .
var K : Key .
op 0 : -> Msg .
op n : Name Fresh -> Nonce [frozen] .
op _*_ : Msg Msg -> Msg [assoc comm frozen] .
---------------Automatically generated and added by Python------------
subsorts Name Nonce Key < Msg .
ops NSL-init NSL-resp : -> Role .
ops DB-init DB-resp : -> Role .
---Used for building the message for the synchronization message.
---op _$;_ : Msg Msg -> Msg [gather(E e) frozen] .
----------End Automatically generated and added by Python-------------------
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
var Z : Msg .
var K : Key .
---Encryption/Decryption Cancellation
eq pk(K,sk(K,Z)) = Z [variant] .
eq sk(K,pk(K,Z)) = Z [variant] .
vars X Y : Msg .
eq X * X = 0 [variant] .
eq X * 0 = X [variant] .
eq X * X * Y = Y [variant] .
endfm
fmod PROTOCOL-SPECIFICATION is
protecting PROTOCOL-EXAMPLE-SYMBOLS . protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
vars A B A1 : Name .
vars NA1 NB : Nonce .
var C : Name .
vars X Y : Msg .
var K : Key .
var NA : Nonce .
var NO : Nonce .
eq STRANDS-DOLEVYAO =
:: nil ::
[ nil |
+(C), nil] &
:: nil ::
[ nil |
-(X),
+(sk(i, X)), nil] &
:: nil ::
[ nil |
-(X),
-(K),
+(pk(K, X)), nil] &
:: nil ::
[ nil |
-(Y),
-(X),
+(X ; Y), nil] &
:: nil ::
[ nil |
-(Y),
-(X),
+(X * Y), nil] &
:: nil ::
[ nil |
-(X ; Y),
+(X), nil] &
:: nil ::
[ nil |
-(X ; Y),
+(Y), nil] &
:: r:Fresh ::
[ nil |
+(n(i, r:Fresh)), nil] [nonexec] .
vars r r' : Fresh .
var N : Nonce .
eq STRANDS-PROTOCOL =
:: r :: [nil | +(pk(B, n(A, r) ; A)),
-(pk(A, n(A, r) ; NB ; B)),
+(pk(B, NB)),
{NSL-init -> DB-resp ;; 1-1 ;; A ; B ; n(A, r)}, nil] &
:: r :: [nil | -(pk(B, NA ; A)),
+(pk(A, NA ; n(B, r) ; B)),
-(pk(B, n(B,r))),
{NSL-resp -> DB-init ;; 1-1 ;; A ; B ; NA}, nil] &
:: r' :: [nil | {NSL-resp -> DB-init ;; 1-1 ;; A ; B ; NA},
+(n(B, r')),
-(NA * n(B, r')), nil] &
:: nil :: [nil | {NSL-init -> DB-resp ;; 1-1 ;; A ; B ; NA },
-(N),
+(NA * N), nil] [nonexec] .
var NC : Nonce .
var D : Name .
eq ATTACK-STATE(0) =
:: r ::
[nil, +(pk(C, n(a, r) ; a)) |
-(pk(a, n(a, r) ; NC ; C)),
+(pk(C, NC)),
{NSL-init -> DB-resp ;; 1-1 ;; a ; C ; n(a, r)}, nil] &
:: r' ::
[nil, {NSL-resp -> DB-init ;; 1-1 ;; D ; b ; n(a, r)},
+(n(b, r')), -(n(a, r) * n(b, r')) | nil]
|| (a != D), (C != b)
|| nil
|| nil
|| nil
[nonexec] .
eq ATTACK-STATE(1) =
:: r ::
[nil, +(pk(b, n(a, r) ; a)),
-(pk(a, n(a, r) ; NC ; b)),
+(pk(b, NC)),
{NSL-init -> DB-resp ;; 1-1 ;; a ; b ; n(a, r)} | nil] &
:: r' ::
[nil, {NSL-resp -> DB-init ;; 1-1 ;; a ; b ; n(a, r)},
+(n(b, r')), -(n(a, r) * n(b, r')) | nil]
|| empty
|| nil
|| nil
|| nil
[nonexec] .
endfm
select MAUDE-NPA .
red genGrammars .
---red run(1, unbounded) .
---red run(0, 13) .
composition_examples/debugging_maude/nsldb_psl.maude deleted 100644 → 0
View file @ 13c634dc
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES . --- -1
sorts Name Nonce Key .
subsort Name < Key .
subsort Name < Public .
subsorts Name Nonce Key < Msg .
ops pk sk : Key Msg -> Msg [frozen] .
op n : Name Fresh -> Nonce [frozen] .
ops a b i : -> Name . --- Alice Bob Intruder
op _;_ : Msg Msg -> Msg [gather frozen (e E)] .
op h : Msg -> Key [frozen] .
var Z : Msg .
var K : Key .
ops a b i : -> Name .
op 0 : -> Msg .
op n : Name Fresh -> Nonce .
op _*_ : Msg Msg -> Msg [assoc comm frozen] .
ops a b i : -> Name .
op 0 : -> Msg .
op n : Name Fresh -> Nonce [frozen] .
op _*_ : Msg Msg -> Msg [assoc comm frozen] .
---------------Automatically generated and added by Python------------
ops nsl-A nsl-B : -> Role .
ops db-A db-B : -> Role .
---Used for building the message for the synchronization message.
op _$;_ : Msg Msg -> Msg [gather(E e) frozen] .
----------End Automatically generated and added by Python-------------------
endfm
fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS .
var Z : Msg .
var K : Key .
---Encryption/Decryption Cancellation
eq pk(K,sk(K,Z)) = Z [variant] .
eq sk(K,pk(K,Z)) = Z [variant] .
vars X Y : Msg .
eq X * X = 0 [variant] .
eq X * 0 = X [variant] .
eq X * X * Y = Y [variant] .
endfm
---Module automatically generated.
fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
vars A B A1 : Name .
vars NA1 NB : Nonce .
var C : Name .
vars X Y : Msg .
var K : Key .
var NA : Nonce .
var NO : Nonce .
eq STRANDS-DOLEVYAO =
:: nil ::
[ nil |
+(C), nil] &
:: nil ::
[ nil |
-(X),
+(sk(i, X)), nil] &
:: nil ::
[ nil |
-(X),
-(K),
+(pk(K, X)), nil] &
:: nil ::
[ nil |
-(Y),
-(X),
+(X ; Y), nil] &
:: nil ::
[ nil |
-(Y),
-(X),
+(X * Y), nil] &
:: nil ::
[ nil |
-(X ; Y),
+(X), nil] &
:: nil ::
[ nil |
-(X ; Y),
+(Y), nil] &
:: r:Fresh ::
[ nil |
+(n(i, r:Fresh)), nil] [nonexec].
eq STRANDS-PROTOCOL =
:: nil ::
[ nil |
{nsl-A -> db-B ;; 1-1 ;; A $; B $; NO},
-(NA),
+(NA * NO), nil] &
:: r:Fresh ::