sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Wed, 19 Apr 2017 17:12:54 +0200
changeset 1723 c93e1ddf1059
parent 1647 f089d9e32e60
child 1724 a2a8ffce4a01
permissions -rw-r--r--
ENGINE-196 ENGINE-197 Sync : fixed group not forming because of checking groupKeys's sender still has same UUID whereas it becomes group's UUID (was working before 52baaf882562, cause group UUID was the one from device)
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);
vb@951
    24
vb@624
    25
        state InitState {
vb@624
    26
            on Init {
edouard@1574
    27
                if deviceGrouped()
vb@624
    28
                    go Grouped;
vb@624
    29
                go Sole;
vb@624
    30
            }
vb@563
    31
        }
vb@563
    32
vb@1409
    33
        state Sole end=1 {
edouard@1523
    34
            on KeyGen
vb@1097
    35
                do sendBeacon;
vb@563
    36
            on CannotDecrypt
edouard@1523
    37
                do sendBeacon;
edouard@1523
    38
            on Beacon(Identity partner){
vb@582
    39
                do sendHandshakeRequest(partner);
edouard@1523
    40
                go SoleBeaconed(partner);
edouard@1523
    41
            }
Edouard@594
    42
            on HandshakeRequest(Identity partner) {
vb@582
    43
                do sendHandshakeRequest(partner);
vb@563
    44
                go HandshakingSole(partner);
vb@563
    45
            }
vb@563
    46
        }
vb@563
    47
edouard@1523
    48
        state SoleBeaconed timeout=600 (Identity expected) {
edouard@1523
    49
            on KeyGen{
edouard@1523
    50
                do sendBeacon;
edouard@1523
    51
                go Sole;
edouard@1523
    52
            }
edouard@1523
    53
            on CannotDecrypt{
edouard@1523
    54
                do sendBeacon;
edouard@1523
    55
                go Sole;
edouard@1523
    56
            }
edouard@1523
    57
            on Beacon(Identity partner) {
edouard@1523
    58
                do sendHandshakeRequest(partner);
edouard@1523
    59
                go SoleBeaconed(partner);
edouard@1523
    60
            }
edouard@1523
    61
            on HandshakeRequest(Identity partner) {
edouard@1523
    62
                if sameIdentities(partner, expected) {
edouard@1523
    63
                    // do nothing, to avoid sending handshake request twice 
edouard@1523
    64
                } else {
edouard@1523
    65
                    do sendHandshakeRequest(partner);
edouard@1523
    66
                }
edouard@1523
    67
                go HandshakingSole(partner);
edouard@1523
    68
            }
edouard@1523
    69
            on Timeout go Sole;
edouard@1523
    70
        }
edouard@1523
    71
edouard@1460
    72
        state HandshakingSole timeout=600 (Identity expected) {
edouard@1477
    73
            on Init{
edouard@1723
    74
                if keyElectionWon(partner) { // TODO : should be "expected"
edouard@1477
    75
                    do notifyInitFormGroup(partner);
edouard@1477
    76
                } else {
edouard@1477
    77
                    do notifyInitAddOurDevice(partner);
edouard@1477
    78
                }
edouard@1477
    79
            }
Edouard@594
    80
            on HandshakeRejected(Identity partner) {
edouard@1523
    81
                do rejectHandshake(partner);
vb@563
    82
                go Sole;
vb@563
    83
            }
Edouard@594
    84
            on HandshakeAccepted(Identity partner) {
edouard@1588
    85
                if sameIdentities(partner, expected) {
edouard@1588
    86
                    do acceptHandshake(partner); 
edouard@1588
    87
                    if keyElectionWon(partner) {
edouard@1588
    88
                        do makeGroup;
edouard@1588
    89
                        do sendGroupKeys(partner);
edouard@1601
    90
                        do renewUUID;
edouard@1588
    91
                        do notifyAcceptedGroupCreated(partner);
edouard@1588
    92
                        go Grouped;
edouard@1588
    93
                    }
edouard@1588
    94
                    go WaitForGroupKeysSole(partner);
vb@563
    95
                }
edouard@1588
    96
                go Sole;
vb@563
    97
            }
edouard@1445
    98
            on Cancel go Sole;
edouard@1597
    99
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1723
   100
                if keyElectionWon(partner) { // TODO : use "expected"
edouard@1601
   101
                    // not suppose to receive groupkeys - ignore
edouard@1601
   102
                } else {
edouard@1723
   103
                    // UUID changes in between, so we can only check for same address and fpr
edouard@1723
   104
                    if sameKeyAndAddress(partner, expected) {
edouard@1601
   105
                        go WaitForAcceptSole(partner, groupkeys);
edouard@1601
   106
                    }
edouard@1596
   107
                }
edouard@1596
   108
            }
edouard@1445
   109
            on Timeout {
edouard@1477
   110
                do notifyTimeout(expected);
edouard@1555
   111
                do sendBeacon;
edouard@1445
   112
                go Sole;
edouard@1445
   113
            }
vb@563
   114
        }
vb@563
   115
    
edouard@1460
   116
        state WaitForGroupKeysSole timeout=600 (Identity expected) {
edouard@1597
   117
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1723
   118
                // UUID changes in between, so we can only check for same address and fpr
edouard@1723
   119
                if sameKeyAndAddress(partner, expected) {
edouard@1597
   120
                    do storeGroupKeys(partner, groupkeys);
edouard@1566
   121
                    do sendGroupUpdate;
edouard@1601
   122
                    do renewUUID;
edouard@1523
   123
                    do notifyAcceptedDeviceAdded(partner);
edouard@1523
   124
                    go Grouped;
edouard@1523
   125
                }
vb@563
   126
            }
edouard@1445
   127
            on Timeout {
edouard@1477
   128
                do notifyTimeout(expected);
vb@569
   129
                go Sole;
vb@569
   130
            }
vb@563
   131
        }
vb@563
   132
edouard@1597
   133
        state WaitForAcceptSole timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   134
            on HandshakeRejected(Identity partner) {
edouard@1596
   135
                do rejectHandshake(partner);
edouard@1596
   136
                go Sole;
edouard@1596
   137
            }
edouard@1596
   138
            on HandshakeAccepted(Identity partner) {
edouard@1723
   139
                // UUID changes in between, so we can only check for same address and fpr
edouard@1723
   140
                if sameKeyAndAddress(partner, expected) {
edouard@1596
   141
                    do acceptHandshake(partner); 
edouard@1597
   142
                    do storeGroupKeys(partner, groupkeys);
edouard@1596
   143
                    do sendGroupUpdate;
edouard@1601
   144
                    do renewUUID;
edouard@1596
   145
                    do notifyAcceptedDeviceAdded(partner);
edouard@1596
   146
                    go Grouped;
edouard@1596
   147
                }
edouard@1647
   148
                go Sole;
edouard@1596
   149
            }
edouard@1596
   150
            on Cancel go Sole;
edouard@1596
   151
            on Timeout {
edouard@1596
   152
                do notifyTimeout(expected);
edouard@1596
   153
                go Sole;
edouard@1596
   154
            }
edouard@1596
   155
        }
edouard@1596
   156
vb@1409
   157
        state Grouped end=1 {
vb@563
   158
            on KeyGen
edouard@1281
   159
                do sendGroupUpdate;
edouard@1586
   160
            on CannotDecrypt {
edouard@1523
   161
                do sendUpdateRequest;
edouard@1586
   162
                do sendBeacon;
edouard@1586
   163
            }
edouard@1297
   164
            on UpdateRequest
edouard@1297
   165
                do sendGroupUpdate;
edouard@1523
   166
            on Beacon(Identity partner){
edouard@1216
   167
                do sendHandshakeRequest(partner);
edouard@1523
   168
                go GroupedBeaconed(partner);
edouard@1523
   169
            }
Edouard@594
   170
            on HandshakeRequest(Identity partner) {
vb@582
   171
                do sendHandshakeRequest(partner);
edouard@1216
   172
                go HandshakingGrouped(partner);
edouard@1216
   173
            }
edouard@1596
   174
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1586
   175
                do storeGroupUpdate(partner, keys);
edouard@1216
   176
        }
edouard@1216
   177
edouard@1523
   178
        state GroupedBeaconed timeout=600 (Identity expected){
edouard@1523
   179
            on KeyGen
edouard@1523
   180
                do sendGroupUpdate;
edouard@1586
   181
            on CannotDecrypt {
edouard@1523
   182
                do sendUpdateRequest;
edouard@1586
   183
                do sendBeacon;
edouard@1586
   184
            }
edouard@1523
   185
            on UpdateRequest
edouard@1523
   186
                do sendGroupUpdate;
edouard@1523
   187
            on Beacon(Identity partner){
edouard@1523
   188
                do sendHandshakeRequest(partner);
edouard@1523
   189
                go GroupedBeaconed(partner);
edouard@1523
   190
            }
edouard@1523
   191
            on HandshakeRequest(Identity partner) {
edouard@1523
   192
                if sameIdentities(partner, expected) {
edouard@1523
   193
                    // do nothing, to avoid sending handshake request twice 
edouard@1523
   194
                } else {
edouard@1523
   195
                    do sendHandshakeRequest(partner);
edouard@1523
   196
                }
edouard@1523
   197
                go HandshakingGrouped(partner);
edouard@1523
   198
            }
edouard@1596
   199
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1588
   200
                do storeGroupUpdate(partner, keys);
edouard@1523
   201
            on Timeout go Grouped;
edouard@1523
   202
        }
edouard@1523
   203
edouard@1460
   204
        state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1586
   205
            // HandshakeRequest from same group are filtered in receive_sync_msg
edouard@1586
   206
            on Init{
edouard@1723
   207
                if keyElectionWon(partner) { // TODO : should be "expected"
edouard@1586
   208
                    do notifyInitAddOtherDevice(partner);
edouard@1586
   209
                } else {
edouard@1586
   210
                    do notifyInitMoveOurDevice(partner);
edouard@1586
   211
                }
edouard@1586
   212
            }
edouard@1216
   213
            on HandshakeRejected(Identity partner) {
edouard@1216
   214
                do rejectHandshake(partner);             // stores rejection of partner
edouard@1626
   215
                do sendGroupUpdate;
edouard@1216
   216
                go Grouped;
vb@563
   217
            }
edouard@1216
   218
            on HandshakeAccepted(Identity partner) {
edouard@1161
   219
                do acceptHandshake(partner); 
edouard@1626
   220
                do sendGroupUpdate;
edouard@1586
   221
                if keyElectionWon(partner) {
edouard@1586
   222
                    do sendGroupKeys(partner);
edouard@1586
   223
                    do notifyAcceptedDeviceAdded(partner);
edouard@1586
   224
                    go Grouped;
edouard@1586
   225
                }
edouard@1586
   226
                go WaitForGroupKeysGrouped(partner);
edouard@1586
   227
            }
edouard@1586
   228
            on Cancel go Grouped;
edouard@1597
   229
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1723
   230
                // TODO : check election  lost, check same address & fpr
edouard@1596
   231
                if sameIdentities(partner, expected) {
edouard@1597
   232
                    go WaitForAcceptGrouped(partner, groupkeys);
edouard@1596
   233
                }
edouard@1596
   234
            }
edouard@1626
   235
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   236
                do notifyOvertaken(partner);
edouard@1626
   237
                do storeGroupUpdate(partner, keys);
edouard@1626
   238
                go Grouped;
edouard@1626
   239
            }
edouard@1586
   240
            on Timeout {
edouard@1586
   241
                do notifyTimeout(expected);
edouard@1445
   242
                go Grouped;
edouard@1445
   243
            }
edouard@1586
   244
        }
edouard@1586
   245
edouard@1586
   246
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1597
   247
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1586
   248
                if sameIdentities(partner, expected) {
edouard@1597
   249
                    do storeGroupKeys(partner, groupkeys);
edouard@1586
   250
                    do sendGroupUpdate;
edouard@1601
   251
                    do renewUUID;
edouard@1586
   252
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   253
                    go Grouped;
edouard@1586
   254
                }
edouard@1586
   255
            }
edouard@1626
   256
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   257
                do notifyOvertaken(partner);
edouard@1626
   258
                do storeGroupUpdate(partner, keys);
edouard@1626
   259
                go Grouped;
edouard@1626
   260
            }
edouard@1445
   261
            on Timeout {
edouard@1477
   262
                do notifyTimeout(expected);
edouard@1216
   263
                go Grouped;
edouard@1161
   264
            }
vb@563
   265
        }
Edouard@613
   266
edouard@1597
   267
        state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   268
            on HandshakeRejected(Identity partner) {
edouard@1596
   269
                do rejectHandshake(partner);
edouard@1626
   270
                do sendGroupUpdate;
edouard@1596
   271
                go Grouped;
edouard@1596
   272
            }
edouard@1596
   273
            on HandshakeAccepted(Identity partner) {
edouard@1647
   274
                if sameIdentities(partner, expected) {
edouard@1647
   275
                    do acceptHandshake(partner); 
edouard@1647
   276
                    do storeGroupKeys(partner, groupkeys);
edouard@1647
   277
                    do sendGroupUpdate;
edouard@1647
   278
                    do renewUUID;
edouard@1647
   279
                    do notifyAcceptedDeviceMoved(partner);
edouard@1647
   280
                }
edouard@1596
   281
                go Grouped;
edouard@1596
   282
            }
edouard@1596
   283
            on Cancel go Grouped;
edouard@1626
   284
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   285
                do notifyOvertaken(partner);
edouard@1626
   286
                do storeGroupUpdate(partner, keys);
edouard@1626
   287
                go Grouped;
edouard@1626
   288
            }
edouard@1596
   289
            on Timeout {
edouard@1596
   290
                do notifyTimeout(expected);
edouard@1596
   291
                go Grouped;
edouard@1596
   292
            }
edouard@1596
   293
        }
edouard@1596
   294
vb@951
   295
        tag Init 1;
vb@951
   296
        tag Beacon 2;
vb@951
   297
        tag HandshakeRequest 3;
vb@951
   298
        tag GroupKeys 4;
Edouard@613
   299
    }
vb@563
   300
}
vb@563
   301