ltv-C-wep.maude 4.69 KB
 acholewa committed May 13, 2015 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 146 147 148 149 150 151 152 153 ``````***( LTV09 paper - protocol C - Wired Equivalent Privacy Protocol Notations: A, B: principals X: any principal (B or the intruder) M1,M2: messages KAB: symmetric key RC4: function modeling the RC4 algorithm (message,symmetric key -> message) v: initial vector used with RC4 (a constant) C: integrity checksum (message -> message) Protocol scheme: 0. A −-> X : v,([M1,C(M1)]*RC4(v,KAX)) 1. A −-> B : v,([M2,C(M2)]*RC4(v,KAB)) where * is the exclusive or operator and exclusive or has the following algebraic properties: X * X = 0 . X * X * Y = Y . X * 0 = X . -------------------- The property to be verified was the secrecy of M2 between A and B. There is an attack: 0.1. A −-> B : v,([M1,C(M1)]*RC4(v,KAB)) 0.2. A −-> I : v,([M1,C(M1)]*RC4(v,KAI)) 1. A −-> I : v,([M2,C(M2)]*RC4(v,KAB)) A fix is to send a different 'v' with every message. [ I have defined 2 separate strands, one just sending a single message as in the actual protocol, the other sending the same payload twice but under different keys, which is legal in this protocol and will be used to break it.] [[[To check the 'fixed version' proposed in the paper, simply change that second strand to use different vectors for each sent message (use neverpattern in attack state, I guess)]]] )*** 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 Vector Key CheckNonce . subsort Name Nonce Null Vector Key CheckNonce < Msg . subsort Name < Public . ops v v2 : -> Vector . op k : Name Name -> Key [frozen] . op rc4 : Vector Key -> Msg [frozen] . op c : Nonce -> CheckNonce [frozen] . op [_,_] : Nonce CheckNonce -> Msg [frozen] . op pair : Vector 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' : Nonce . vars A B C : Name . var V : Vector . eq STRANDS-DOLEVYAO = :: nil :: [ nil | -(X), -(Y), +(X * Y), nil ] & :: nil :: [ nil | -(A), +(k(A,i)), nil ] & :: nil :: [ nil | -(pair(V, X)), +(V), nil ] & :: nil :: [ nil | -(pair(V, X)), +(X), nil ] & :: nil :: [ nil | -(V), -(k(A,B)), +(rc4(V,k(A,B))), nil ] & :: nil :: [ nil | -(N), +(c(N)), nil ] & :: nil :: [ nil | -([N,c(N')]), +(N), nil ] & :: nil :: [ nil | +(null), nil ] & :: nil :: [ nil | +(A), nil ] [nonexec] . eq STRANDS-PROTOCOL = :: r :: [nil | +(pair(V, ([n(A,r), c(n(A,r))] * rc4(V,k(A,B))))), nil] & :: r' :: [nil | +(pair(V, ([n(A,r'), c(n(A,r'))] * rc4(V,k(A,B))))), +(pair(V, ([n(A,r'), c(n(A,r'))] * rc4(V,k(A,C))))), nil] [nonexec] . eq ATTACK-STATE(0) = :: r :: [nil, +(pair(v, ([n(a,r), c(n(a,r))] * rc4(v,k(a,b))))) | 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 .``````