Commit a9b9168a authored by Joy Mitra's avatar Joy Mitra
Browse files

tesla changes

parent dc845e96
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 diff is collapsed.
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 diff is collapsed.
***(
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
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7.1 built: Jun 27 2016 16:43:23
Copyright 1997-2016 SRI International
Thu Aug 10 12:14:58 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
==========================================
reduce in MAUDE-NPA : genGrammars .
rewrites: 5056483 in 6927ms cpu (7053ms real) (729962 rewrites/second)
result GrammarList: (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ;
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl #0:Msg notInI,
#0:Msg notLeq n(#1:Name, #2:Fresh) => (#0:Msg ; #3:Msg) inL . ;
grl #0:Msg notInI,
#0:Msg notLeq n(#1:Name, #2:Fresh) => (#3:Name ; #0:Msg) inL . )
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ;
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl #0:Msg notInI,
(#0:Msg notLeq n(#1:Name, #2:Fresh)),
#0:Msg notLeq n(#3:Name, #4:Fresh) ; #3:Name => (#5:Msg ; #0:Msg) inL . )
| (errorNoHeuristicApplied {
grl empty => (#1:Msg ; #2:Msg) inL . ,none,
grl empty => (#1:Msg,#2:Msg) inL . ,none,
grl empty => (#1:Msg,#2:Msg) inL . } usingGrammar
grl empty => (#1:Msg ; #2:Msg) inL . )
| (errorInconsistentExceptionsInGrammarRule
grl n(#0:Name, #1:Fresh) notLeq #1:Nonce => n(#0:Name, #1:Fresh) inL . inGrammar
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl #5:Msg inL => pk(#3:Name, #5:Msg) inL . ;
grl n(#0:Name, #1:Fresh) notLeq #1:Nonce => n(#0:Name, #1:Fresh) inL . )
| (errorNoHeuristicApplied {
grl #50:Key notInI => pk(#50:Key, #60:Msg) inL . ,none,
grl #50:Key notInI => #60:Msg inL . ,none,
grl #50:Key notInI => #60:Msg inL . } usingGrammar
grl #50:Key notInI => pk(#50:Key, #60:Msg) inL . )
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ;
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl #0:Msg notInI,
(#0:Msg notLeq #1:Nonce),
(#0:Msg notLeq #2:Name ; n(#2:Name, #3:Fresh)),
#0:Msg notLeq #4:Nonce ; n(#5:Name, #6:Fresh) ; #5:Name => pk(#7:Key, #0:Msg) inL . )
| (errorNoHeuristicApplied {
grl empty => pk(#1:Key, #2:Msg) inL . ,none,
grl empty => #2:Msg inL . ,none,
grl empty => #2:Msg inL . } usingGrammar
grl empty => pk(#1:Key, #2:Msg) inL . )
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ;
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl #0:Key notInI,
#0:Key notLeq i => sk(#0:Key, #1:Msg) inL . )
| (
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ;
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl #0:Msg notInI => sk(#1:Key, #0:Msg) inL . )
|
grl #0:Msg inL => pk(#1:Name, #0:Msg) inL . ;
grl #0:Msg inL => sk(#1:Key, #0:Msg) inL . ;
grl #0:Msg inL => (#1:Msg ; #0:Msg) inL . ;
grl #0:Msg inL => (#0:Msg ; #1:Msg) inL . ;
grl sk(#0:Key, #1:Msg) notLeq sk(i, #2:Msg) => sk(#0:Key, #1:Msg) inL .
==========================================
reduce in MAUDE-NPA : run(0) .
rewrites: 5818 in 94ms cpu (97ms real) (61532 rewrites/second)
result ShortIdSystem: < 1 >
:: r:Fresh ::
[ nil,
-(pk(b, a ; N:Nonce)),
+(pk(a, N:Nonce ; n(b, r:Fresh) ; b)) |
-(pk(b, n(b, r:Fresh))), nil]
|
pk(b, n(b, r:Fresh)) inI,
n(b, r:Fresh) inI
|
-(pk(b, n(b, r:Fresh)))
|
nil
==========================================
reduce in MAUDE-NPA : summary(1) .
rewrites: 557922 in 731ms cpu (750ms real) (763203 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2) .
rewrites: 1080519 in 1425ms cpu (1447ms real) (757856 rewrites/second)
result Summary: States>> 7 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(3) .
rewrites: 2068326 in 2683ms cpu (2712ms real) (770717 rewrites/second)
result Summary: States>> 6 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(4) .
rewrites: 1801398 in 2735ms cpu (2758ms real) (658641 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(5) .