sync/devicegroup.fsm
author Krista Bennett <krista@pep-project.org>
Mon, 20 Nov 2017 16:04:50 +0100
branchENGINE-289
changeset 2287 026ab4dae779
parent 1739 73374beaca6f
parent 2271 25bfd109320c
permissions -rw-r--r--
merged in default
krista@2271
     1
// This file is under GNU General Public License 3.0
krista@2271
     2
// see LICENSE.txt
krista@2271
     3
krista@2271
     4
// DeviceGroup protocol for p≡p
krista@2271
     5
krista@2271
     6
// Copyleft (c) 2016, p≡p foundation
krista@2271
     7
krista@2271
     8
// Written by Volker Birk
krista@2271
     9
krista@2271
    10
include ./fsm.yml2
krista@2271
    11
krista@2271
    12
protocol DeviceGroup {
krista@2271
    13
    // all messages have a timestamp, time out and are removed after timeout
krista@2271
    14
krista@2271
    15
    broadcast sendBeacon;
krista@2271
    16
    broadcast sendGroupUpdate;
krista@2271
    17
    broadcast sendUpdateRequest;
krista@2271
    18
    unencrypted sendBeacon;
krista@2271
    19
krista@2271
    20
    fsm DeviceState filename=sync {
krista@2271
    21
        condition deviceGrouped();
krista@2271
    22
        condition keyElectionWon(Identity partner);
krista@2271
    23
        condition sameIdentities(Identity a, Identity b);
krista@2271
    24
        condition sameKeyAndAddress(Identity a, Identity b);
krista@2271
    25
krista@2271
    26
        state InitState {
krista@2271
    27
            on Init {
krista@2271
    28
                if deviceGrouped()
krista@2271
    29
                    go Grouped;
krista@2271
    30
                go Sole;
krista@2271
    31
            }
krista@2271
    32
        }
krista@2271
    33
krista@2271
    34
        state Sole end=1 {
krista@2271
    35
            on KeyGen {
krista@2271
    36
                do sendBeacon;
krista@2271
    37
                go SoleWaiting;
krista@2271
    38
            }
krista@2271
    39
            on CannotDecrypt {
krista@2271
    40
                do sendBeacon;
krista@2271
    41
                go SoleWaiting;
krista@2271
    42
            }
krista@2271
    43
            on Beacon(Identity partner){
krista@2271
    44
                do sendHandshakeRequest(partner);
krista@2271
    45
                go SoleBeaconed(partner);
krista@2271
    46
            }
krista@2271
    47
            on HandshakeRequest(Identity partner) {
krista@2271
    48
                do sendHandshakeRequest(partner);
krista@2271
    49
                go HandshakingSole(partner);
krista@2271
    50
            }
krista@2271
    51
        }
krista@2271
    52
krista@2271
    53
        // copy of sole state with a timeout to enable fast polling for a second
krista@2271
    54
        // TODO use more YSLT power here (substates ?) 
krista@2271
    55
        state SoleWaiting timeout=60 {
krista@2271
    56
            on KeyGen {
krista@2271
    57
                do sendBeacon;
krista@2271
    58
            }
krista@2271
    59
            on CannotDecrypt {
krista@2271
    60
                do sendBeacon;
krista@2271
    61
            }
krista@2271
    62
            on Beacon(Identity partner){
krista@2271
    63
                do sendHandshakeRequest(partner);
krista@2271
    64
                go SoleBeaconed(partner);
krista@2271
    65
            }
krista@2271
    66
            on HandshakeRequest(Identity partner) {
krista@2271
    67
                do sendHandshakeRequest(partner);
krista@2271
    68
                go HandshakingSole(partner);
krista@2271
    69
            }
krista@2271
    70
            on Timeout go Sole;
krista@2271
    71
        }
krista@2271
    72
krista@2271
    73
        state SoleBeaconed timeout=600 (Identity expected) {
krista@2271
    74
            on KeyGen{
krista@2271
    75
                do sendBeacon;
krista@2271
    76
                go Sole;
krista@2271
    77
            }
krista@2271
    78
            on CannotDecrypt{
krista@2271
    79
                do sendBeacon;
krista@2271
    80
                go Sole;
krista@2271
    81
            }
krista@2271
    82
            on Beacon(Identity partner) {
krista@2271
    83
                do sendHandshakeRequest(partner);
krista@2271
    84
                go SoleBeaconed(partner);
krista@2271
    85
            }
krista@2271
    86
            on HandshakeRequest(Identity partner) {
krista@2271
    87
                if sameIdentities(partner, expected) {
krista@2271
    88
                    // do nothing, to avoid sending handshake request twice 
krista@2271
    89
                } else {
krista@2271
    90
                    do sendHandshakeRequest(partner);
krista@2271
    91
                }
krista@2271
    92
                go HandshakingSole(partner);
krista@2271
    93
            }
krista@2271
    94
            on Timeout go Sole;
krista@2271
    95
        }
krista@2271
    96
krista@2271
    97
        state HandshakingSole timeout=600 (Identity expected) {
krista@2271
    98
            on Init{
krista@2271
    99
                if keyElectionWon(expected) {
krista@2271
   100
                    do notifyInitFormGroup(expected);
krista@2271
   101
                } else {
krista@2271
   102
                    do notifyInitAddOurDevice(expected);
krista@2271
   103
                }
krista@2271
   104
            }
krista@2271
   105
            on HandshakeRejected(Identity partner) {
krista@2271
   106
                do rejectHandshake(partner);
krista@2271
   107
                go Sole;
krista@2271
   108
            }
krista@2271
   109
            on HandshakeAccepted(Identity partner) {
krista@2271
   110
                if sameIdentities(partner, expected) {
krista@2271
   111
                    do acceptHandshake(partner); 
krista@2271
   112
                    if keyElectionWon(partner) {
krista@2271
   113
                        do makeGroup;
krista@2271
   114
                        do sendGroupKeys(partner);
krista@2271
   115
                        do renewUUID;
krista@2271
   116
                        do notifyAcceptedGroupCreated(partner);
krista@2271
   117
                        go Grouped;
krista@2271
   118
                    }
krista@2271
   119
                    go WaitForGroupKeysSole(partner);
krista@2271
   120
                }
krista@2271
   121
                go Sole;
krista@2271
   122
            }
krista@2271
   123
            on Cancel go Sole;
krista@2271
   124
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
krista@2271
   125
                if keyElectionWon(expected) {
krista@2271
   126
                    // not supposed to receive groupkeys - ignore
krista@2271
   127
                } else {
krista@2271
   128
                    // UUID changes in between, so we can only check for same address and fpr
krista@2271
   129
                    if sameKeyAndAddress(partner, expected) {
krista@2271
   130
                        go WaitForAcceptSole(partner, groupkeys);
krista@2271
   131
                    }
krista@2271
   132
                }
krista@2271
   133
            }
krista@2271
   134
            on Timeout {
krista@2271
   135
                do notifyTimeout(expected);
krista@2271
   136
                do sendBeacon;
krista@2271
   137
                go Sole;
krista@2271
   138
            }
krista@2271
   139
        }
krista@2271
   140
    
krista@2271
   141
        state WaitForGroupKeysSole timeout=600 (Identity expected) {
krista@2271
   142
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
krista@2271
   143
                // UUID changes in between, so we can only check for same address and fpr
krista@2271
   144
                if sameKeyAndAddress(partner, expected) {
krista@2271
   145
                    do storeGroupKeys(partner, groupkeys);
krista@2271
   146
                    do sendGroupUpdate;
krista@2271
   147
                    do renewUUID;
krista@2271
   148
                    do notifyAcceptedDeviceAdded(partner);
krista@2271
   149
                    go Grouped;
krista@2271
   150
                }
krista@2271
   151
            }
krista@2271
   152
            on Timeout {
krista@2271
   153
                do notifyTimeout(expected);
krista@2271
   154
                go Sole;
krista@2271
   155
            }
krista@2271
   156
        }
krista@2271
   157
krista@2271
   158
        state WaitForAcceptSole timeout=600 (Identity expected, GroupKeys groupkeys) {
krista@2271
   159
            on HandshakeRejected(Identity partner) {
krista@2271
   160
                do rejectHandshake(partner);
krista@2271
   161
                go Sole;
krista@2271
   162
            }
krista@2271
   163
            on HandshakeAccepted(Identity partner) {
krista@2271
   164
                // UUID changes in between, so we can only check for same address and fpr
krista@2271
   165
                if sameKeyAndAddress(partner, expected) {
krista@2271
   166
                    do acceptHandshake(partner); 
krista@2271
   167
                    do storeGroupKeys(partner, groupkeys);
krista@2271
   168
                    do sendGroupUpdate;
krista@2271
   169
                    do renewUUID;
krista@2271
   170
                    do notifyAcceptedDeviceAdded(partner);
krista@2271
   171
                    go Grouped;
krista@2271
   172
                }
krista@2271
   173
                go Sole;
krista@2271
   174
            }
krista@2271
   175
            on Cancel go Sole;
krista@2271
   176
            on Timeout {
krista@2271
   177
                do notifyTimeout(expected);
krista@2271
   178
                go Sole;
krista@2271
   179
            }
krista@2271
   180
        }
krista@2271
   181
krista@2271
   182
        state Grouped end=1 {
krista@2271
   183
            on KeyGen
krista@2271
   184
                do sendGroupUpdate;
krista@2271
   185
            on CannotDecrypt {
krista@2271
   186
                do sendUpdateRequest;
krista@2271
   187
                do sendBeacon;
krista@2271
   188
                go GroupWaiting;
krista@2271
   189
            }
krista@2271
   190
            on UpdateRequest
krista@2271
   191
                do sendGroupUpdate;
krista@2271
   192
            on Beacon(Identity partner){
krista@2271
   193
                do sendHandshakeRequest(partner);
krista@2271
   194
                go GroupedBeaconed(partner);
krista@2271
   195
            }
krista@2271
   196
            on HandshakeRequest(Identity partner) {
krista@2271
   197
                do sendHandshakeRequest(partner);
krista@2271
   198
                go HandshakingGrouped(partner);
krista@2271
   199
            }
krista@2271
   200
            on GroupUpdate(Identity partner, IdentityList keys)
krista@2271
   201
                do storeGroupUpdate(partner, keys);
krista@2271
   202
        }
krista@2271
   203
krista@2271
   204
        // copy of grouped state, with a timeout to enable fast poling for a minut
krista@2271
   205
        state GroupWaiting timeout=60 {
krista@2271
   206
            on KeyGen
krista@2271
   207
                do sendGroupUpdate;
krista@2271
   208
            on CannotDecrypt {
krista@2271
   209
                do sendUpdateRequest;
krista@2271
   210
                do sendBeacon;
krista@2271
   211
            }
krista@2271
   212
            on UpdateRequest
krista@2271
   213
                do sendGroupUpdate;
krista@2271
   214
            on Beacon(Identity partner){
krista@2271
   215
                do sendHandshakeRequest(partner);
krista@2271
   216
                go GroupedBeaconed(partner);
krista@2271
   217
            }
krista@2271
   218
            on HandshakeRequest(Identity partner) {
krista@2271
   219
                do sendHandshakeRequest(partner);
krista@2271
   220
                go HandshakingGrouped(partner);
krista@2271
   221
            }
krista@2271
   222
            on GroupUpdate(Identity partner, IdentityList keys)
krista@2271
   223
                do storeGroupUpdate(partner, keys);
krista@2271
   224
            on Timeout go Grouped;
krista@2271
   225
        }
krista@2271
   226
krista@2271
   227
        state GroupedBeaconed timeout=600 (Identity expected){
krista@2271
   228
            on KeyGen
krista@2271
   229
                do sendGroupUpdate;
krista@2271
   230
            on CannotDecrypt {
krista@2271
   231
                do sendUpdateRequest;
krista@2271
   232
                do sendBeacon;
krista@2271
   233
            }
krista@2271
   234
            on UpdateRequest
krista@2271
   235
                do sendGroupUpdate;
krista@2271
   236
            on Beacon(Identity partner){
krista@2271
   237
                do sendHandshakeRequest(partner);
krista@2271
   238
                go GroupedBeaconed(partner);
krista@2271
   239
            }
krista@2271
   240
            on HandshakeRequest(Identity partner) {
krista@2271
   241
                if sameIdentities(partner, expected) {
krista@2271
   242
                    // do nothing, to avoid sending handshake request twice 
krista@2271
   243
                } else {
krista@2271
   244
                    do sendHandshakeRequest(partner);
krista@2271
   245
                }
krista@2271
   246
                go HandshakingGrouped(partner);
krista@2271
   247
            }
krista@2271
   248
            on GroupUpdate(Identity partner, IdentityList keys)
krista@2271
   249
                do storeGroupUpdate(partner, keys);
krista@2271
   250
            on Timeout go Grouped;
krista@2271
   251
        }
krista@2271
   252
krista@2271
   253
        state HandshakingGrouped timeout=600 (Identity expected) {
krista@2271
   254
            // HandshakeRequest from same group are filtered in receive_sync_msg
krista@2271
   255
            on Init{
krista@2271
   256
                if keyElectionWon(expected) {
krista@2271
   257
                    do notifyInitAddOtherDevice(partner);
krista@2271
   258
                } else {
krista@2271
   259
                    do notifyInitMoveOurDevice(partner);
krista@2271
   260
                }
krista@2271
   261
            }
krista@2271
   262
            on HandshakeRejected(Identity partner) {
krista@2271
   263
                do rejectHandshake(partner);             // stores rejection of partner
krista@2271
   264
                do sendGroupUpdate;
krista@2271
   265
                go Grouped;
krista@2271
   266
            }
krista@2271
   267
            on HandshakeAccepted(Identity partner) {
krista@2271
   268
                do acceptHandshake(partner); 
krista@2271
   269
                do sendGroupUpdate;
krista@2271
   270
                if keyElectionWon(partner) {
krista@2271
   271
                    do sendGroupKeys(partner);
krista@2271
   272
                    do notifyAcceptedDeviceAdded(partner);
krista@2271
   273
                    go Grouped;
krista@2271
   274
                }
krista@2271
   275
                go WaitForGroupKeysGrouped(partner);
krista@2271
   276
            }
krista@2271
   277
            on Cancel go Grouped;
krista@2271
   278
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
krista@2271
   279
                if keyElectionWon(expected) {
krista@2271
   280
                    // not supposed to receive groupkeys - ignore
krista@2271
   281
                } else {
krista@2271
   282
                    // UUID changes in between, so we can only check for same address and fpr
krista@2271
   283
                    if sameKeyAndAddress(partner, expected) {
krista@2271
   284
                        go WaitForAcceptGrouped(partner, groupkeys);
krista@2271
   285
                    }
krista@2271
   286
                }
krista@2271
   287
            }
krista@2271
   288
            on GroupUpdate(Identity partner, IdentityList keys) {
krista@2271
   289
                do notifyOvertaken(partner);
krista@2271
   290
                do storeGroupUpdate(partner, keys);
krista@2271
   291
                go Grouped;
krista@2271
   292
            }
krista@2271
   293
            on Timeout {
krista@2271
   294
                do notifyTimeout(expected);
krista@2271
   295
                go Grouped;
krista@2271
   296
            }
krista@2271
   297
        }
krista@2271
   298
krista@2271
   299
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
krista@2271
   300
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
krista@2271
   301
                if sameIdentities(partner, expected) {
krista@2271
   302
                    do storeGroupKeys(partner, groupkeys);
krista@2271
   303
                    do sendGroupUpdate;
krista@2271
   304
                    do renewUUID;
krista@2271
   305
                    do notifyAcceptedDeviceMoved(partner);
krista@2271
   306
                    go Grouped;
krista@2271
   307
                }
krista@2271
   308
            }
krista@2271
   309
            on GroupUpdate(Identity partner, IdentityList keys) {
krista@2271
   310
                do notifyOvertaken(partner);
krista@2271
   311
                do storeGroupUpdate(partner, keys);
krista@2271
   312
                go Grouped;
krista@2271
   313
            }
krista@2271
   314
            on Timeout {
krista@2271
   315
                do notifyTimeout(expected);
krista@2271
   316
                go Grouped;
krista@2271
   317
            }
krista@2271
   318
        }
krista@2271
   319
krista@2271
   320
        state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
krista@2271
   321
            on HandshakeRejected(Identity partner) {
krista@2271
   322
                do rejectHandshake(partner);
krista@2271
   323
                do sendGroupUpdate;
krista@2271
   324
                go Grouped;
krista@2271
   325
            }
krista@2271
   326
            on HandshakeAccepted(Identity partner) {
krista@2271
   327
                if sameIdentities(partner, expected) {
krista@2271
   328
                    do acceptHandshake(partner); 
krista@2271
   329
                    do storeGroupKeys(partner, groupkeys);
krista@2271
   330
                    do sendGroupUpdate;
krista@2271
   331
                    do renewUUID;
krista@2271
   332
                    do notifyAcceptedDeviceMoved(partner);
krista@2271
   333
                }
krista@2271
   334
                go Grouped;
krista@2271
   335
            }
krista@2271
   336
            on Cancel go Grouped;
krista@2271
   337
            on GroupUpdate(Identity partner, IdentityList keys) {
krista@2271
   338
                do notifyOvertaken(partner);
krista@2271
   339
                do storeGroupUpdate(partner, keys);
krista@2271
   340
                go Grouped;
krista@2271
   341
            }
krista@2271
   342
            on Timeout {
krista@2271
   343
                do notifyTimeout(expected);
krista@2271
   344
                go Grouped;
krista@2271
   345
            }
krista@2271
   346
        }
krista@2271
   347
krista@2271
   348
        tag Init 1;
krista@2271
   349
        tag Beacon 2;
krista@2271
   350
        tag HandshakeRequest 3;
krista@2271
   351
        tag GroupKeys 4;
krista@2271
   352
    }
krista@2271
   353
}
krista@2271
   354