nspk.maude 2.21 KB
Newer Older
Joy Mitra's avatar
Joy Mitra committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES .
sorts Name  Nonce  Enc .
subsorts Name < Public .
op pk : Name  Msg -> 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 pk ( X:Name , sk ( X:Name , Z:Msg ) ) = Z:Msg [ variant ] .
eq sk ( X:Name , pk ( X:Name , Z:Msg ) ) = Z:Msg [ variant ] .
endfm
fmod PROTOCOL-SPECIFICATION is protecting PROTOCOL-EXAMPLE-SYMBOLS .
protecting DEFINITION-PROTOCOL-RULES .
protecting DEFINITION-CONSTRAINTS-INPUT .
Joy Mitra's avatar
Joy Mitra committed
20
eq STRANDS-DOLEVYAO = 
Joy Mitra's avatar
Joy Mitra committed
21
:: nil ::
Joy Mitra's avatar
Joy Mitra committed
22 23 24
[ nil | 
   -(X:Msg), 
   +(sk(i, X:Msg)), nil]  & 
Joy Mitra's avatar
Joy Mitra committed
25
:: nil ::
Joy Mitra's avatar
Joy Mitra committed
26 27 28 29
[ nil | 
   -(Y:Msg), 
   -(X:Msg), 
   +(X:Msg ; Y:Msg), nil]  & 
Joy Mitra's avatar
Joy Mitra committed
30
:: nil ::
Joy Mitra's avatar
Joy Mitra committed
31 32 33 34
[ nil | 
   -(A:Name), 
   -(X:Msg), 
   +(pk(A:Name, X:Msg)), nil]  & 
Joy Mitra's avatar
Joy Mitra committed
35
:: nil ::
Joy Mitra's avatar
Joy Mitra committed
36 37 38
[ nil | 
   -(X:Msg ; Y:Msg), 
   +(X:Msg), nil]  & 
Joy Mitra's avatar
Joy Mitra committed
39
:: nil ::
Joy Mitra's avatar
Joy Mitra committed
40 41 42
[ nil | 
   -(X:Msg ; Y:Msg), 
   +(Y:Msg), nil]  & 
Joy Mitra's avatar
Joy Mitra committed
43
:: r1:Fresh ::
Joy Mitra's avatar
Joy Mitra committed
44
[ nil | 
Joy Mitra's avatar
Joy Mitra committed
45
   +(n(i, r1:Fresh)), nil] [nonexec].
Joy Mitra's avatar
Joy Mitra committed
46
eq STRANDS-PROTOCOL = 
Joy Mitra's avatar
Joy Mitra committed
47
:: r1:Fresh ::
Joy Mitra's avatar
Joy Mitra committed
48 49 50 51
[ 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]  & 
Joy Mitra's avatar
Joy Mitra committed
52
:: r2:Fresh ::
Joy Mitra's avatar
Joy Mitra committed
53 54 55
[ nil | 
   -(pk(BName:Name, AName:Name ; N1:Nonce)), 
   +(pk(AName:Name, N1:Nonce ; n(BName:Name, r2:Fresh))), 
Joy Mitra's avatar
Joy Mitra committed
56
   -(pk(BName:Name, n(BName:Name, r2:Fresh))), nil] [nonexec].
Joy Mitra's avatar
Joy Mitra committed
57
var LIST : SMsgList-R . var K : IntruderKnowledge . var S : StrandSet . eq ATTACK-STATE(0)= 
Joy Mitra's avatar
Joy Mitra committed
58
:: r2:Fresh ::
Joy Mitra's avatar
Joy Mitra committed
59 60 61 62 63
[ nil, 
   -(pk(b, a ; N1:Nonce)), 
   +(pk(a, N1:Nonce ; n(b, r2:Fresh))), 
   -(pk(b, n(b, r2:Fresh))) | nil] 
|| 
Joy Mitra's avatar
Joy Mitra committed
64
n(b, r2:Fresh) inI
Joy Mitra's avatar
Joy Mitra committed
65
|| 
Joy Mitra's avatar
Joy Mitra committed
66
nil
Joy Mitra's avatar
Joy Mitra committed
67
|| 
Joy Mitra's avatar
Joy Mitra committed
68
nil
Joy Mitra's avatar
Joy Mitra committed
69
|| 
Joy Mitra's avatar
Joy Mitra committed
70
nil[nonexec].
Joy Mitra's avatar
Joy Mitra committed
71
 eq ATTACK-STATE(1)= 
Joy Mitra's avatar
Joy Mitra committed
72
:: r2:Fresh ::
Joy Mitra's avatar
Joy Mitra committed
73 74 75 76 77
[ nil, 
   -(pk(b, a ; N1:Nonce)), 
   +(pk(a, N1:Nonce ; n(b, r2:Fresh))), 
   -(pk(b, n(b, r2:Fresh))) | nil] 
|| 
Joy Mitra's avatar
Joy Mitra committed
78
n(b, r2:Fresh) inI
Joy Mitra's avatar
Joy Mitra committed
79
|| 
Joy Mitra's avatar
Joy Mitra committed
80
nil
Joy Mitra's avatar
Joy Mitra committed
81
|| 
Joy Mitra's avatar
Joy Mitra committed
82
nil
Joy Mitra's avatar
Joy Mitra committed
83
|| never((S & 
Joy Mitra's avatar
Joy Mitra committed
84
:: r1:Fresh ::
Joy Mitra's avatar
Joy Mitra committed
85 86 87
[ nil, 
   +(pk(b, a ; n(a, r1:Fresh))), 
   -(pk(a, n(a, r1:Fresh) ; N2:Nonce)), 
Joy Mitra's avatar
Joy Mitra committed
88 89
   +(pk(b, N2:Nonce)) | nil] ) || K)[nonexec].
 endfm
Joy Mitra's avatar
Joy Mitra committed
90
select MAUDE-NPA .