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