ltv-F-tmn.maude 4.11 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
***(
LTV09 paper - protocol F - TMN
Notations: 
A, B, S : principals
KA,KB: fresh symmetric keys 
PKS: public key of the server
Protocol scheme:
1. A −-> S : B,{KA}PKS
2. S −-> B : A
3. B −-> S : A,{KB}PKS
4. S −-> A : B, KB * KA

----
the attack:
1. A −-> S : B,{KA}PKS 
2. S −-> I : A
3. I(B) −-> S : A,{KI}PKS
4. S −-> I : B, KI * KA
In the first step, A starts a normal session with B. In the second step, I intercepts the message sent by S and then, in step 3, he impersonates B and sends his own symmetric key to the server. Finally, the intruder intercepts B and KI ⊕ KA and as he knows KI, he can find KA by computing (KI ⊕ KA) ⊕ KI . Finally, I can transmit B, KI ⊕ KA to A.

CODE BELOW IS FROM ANOTHER FILE AS TEMPLATE!!! CHANGE everything!
)***

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 Null .
  subsort Name Nonce Null < Msg .
  subsort Name < Public .

op pair : Msg Msg -> Msg [frozen] .
*** encryption here is thus that only the server can decrypt it!
op enc : Msg -> Msg [frozen] .

  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .
  
  --- Principals
  op a : -> Name . --- Alice
  op b : -> Name . --- Bob
  op i : -> Name . --- Intruder
  
  --- XOR operator
  op _*_ : Msg Msg -> Msg [frozen assoc comm] .
  op null : -> Msg .

endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  
  ----------------------------------------------------------
  --- Overwrite this module with the algebraic properties 
  --- of your protocol
  ----------------------------------------------------------

  *** Exclusive or properties
  eq X:Msg * X:Msg = null [variant] .
  eq X:Msg * X:Msg * Y:Msg = Y:Msg [variant] .
  eq X:Msg * null = X: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 X Y  : Msg .
  vars r r' : Fresh .
  vars N N' NA NB : Nonce .
  vars A B C : Name .

  eq STRANDS-DOLEVYAO
   = :: nil :: [ nil | -(X), -(Y), +(X * Y), nil ] &
     :: nil :: [ nil | -(pair(X,Y)), +(X), nil ] &
     :: nil :: [ nil | -(pair(X,Y)), +(Y), nil ] &
     :: nil :: [ nil | -(X), -(Y), +(pair(X,Y)), nil ] &
     :: r   :: [ nil | +(n(i, r)), nil ] &
     :: nil :: [ nil | -(N), +(enc(N)), nil ] &
     :: nil :: [ nil | +(A), nil ] &
     :: nil :: [ nil | +(null), nil ]
  [nonexec] .

  eq STRANDS-PROTOCOL
  = *** A
    :: r :: 
    [nil | +(pair(B, enc(n(A,r)))),
           -(pair(B, n(A,r) * NB)), 
           nil] 
    &
    *** B
    :: r' :: 
    [nil | -(A),
           +(pair(A, enc(n(B,r')))),
           nil] 
    &
    *** S
    :: nil ::
    [nil | -(pair(B, enc(NA))),
           +(A),
           -(pair(A, enc(NB))),
           +(pair(B, NA * NB)), 
           nil] 
    
  [nonexec] .

  eq ATTACK-STATE(0)
   = 
    :: r :: 
    [nil,  +(pair(b, enc(n(a,r)))),
           -(pair(b, n(a,r) * NB)) | nil]
     || n(a,r) inI, empty
     || nil
     || nil
     || nil
  [nonexec] .

  ----------------------------------------------------------
  --- Grammars for co-invariant generation
  --- Keyword GENERATED-GRAMMARS -> seed terms for grammar generation 
  --- (if not, use automaticly generated seed terms)
  --- Keyword EXTRA-GRAMMARS -> seed terms for grammar generation 
  --- apart of automaticly generated ones
  --- Format of seed terms (grl Conditions => Term inL .) ! S1/S2
  ----------------------------------------------------------

endfm

--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .