sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Mon, 13 Mar 2017 14:33:17 +0100
branchENGINE-188
changeset 1647 f089d9e32e60
parent 1626 22343c95398a
child 1669 99c54cb90ff3
child 1723 c93e1ddf1059
permissions -rw-r--r--
ENGINE-188 brutal fixes so that last mp_sync_test.py still completes. closing that branch
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@1523
    74
                if keyElectionWon(partner) {
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@1601
   100
                if keyElectionWon(partner) {
edouard@1601
   101
                    // not suppose to receive groupkeys - ignore
edouard@1601
   102
                } else {
edouard@1601
   103
                    if sameIdentities(partner, expected) {
edouard@1601
   104
                        go WaitForAcceptSole(partner, groupkeys);
edouard@1601
   105
                    }
edouard@1596
   106
                }
edouard@1596
   107
            }
edouard@1445
   108
            on Timeout {
edouard@1477
   109
                do notifyTimeout(expected);
edouard@1555
   110
                do sendBeacon;
edouard@1445
   111
                go Sole;
edouard@1445
   112
            }
vb@563
   113
        }
vb@563
   114
    
edouard@1460
   115
        state WaitForGroupKeysSole timeout=600 (Identity expected) {
edouard@1597
   116
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1523
   117
                if sameIdentities(partner, expected) {
edouard@1597
   118
                    do storeGroupKeys(partner, groupkeys);
edouard@1566
   119
                    do sendGroupUpdate;
edouard@1601
   120
                    do renewUUID;
edouard@1523
   121
                    do notifyAcceptedDeviceAdded(partner);
edouard@1523
   122
                    go Grouped;
edouard@1523
   123
                }
vb@563
   124
            }
edouard@1445
   125
            on Timeout {
edouard@1477
   126
                do notifyTimeout(expected);
vb@569
   127
                go Sole;
vb@569
   128
            }
vb@563
   129
        }
vb@563
   130
edouard@1597
   131
        state WaitForAcceptSole timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   132
            on HandshakeRejected(Identity partner) {
edouard@1596
   133
                do rejectHandshake(partner);
edouard@1596
   134
                go Sole;
edouard@1596
   135
            }
edouard@1596
   136
            on HandshakeAccepted(Identity partner) {
edouard@1596
   137
                if sameIdentities(partner, expected) {
edouard@1596
   138
                    do acceptHandshake(partner); 
edouard@1597
   139
                    do storeGroupKeys(partner, groupkeys);
edouard@1596
   140
                    do sendGroupUpdate;
edouard@1601
   141
                    do renewUUID;
edouard@1596
   142
                    do notifyAcceptedDeviceAdded(partner);
edouard@1596
   143
                    go Grouped;
edouard@1596
   144
                }
edouard@1647
   145
                go Sole;
edouard@1596
   146
            }
edouard@1596
   147
            on Cancel go Sole;
edouard@1596
   148
            on Timeout {
edouard@1596
   149
                do notifyTimeout(expected);
edouard@1596
   150
                go Sole;
edouard@1596
   151
            }
edouard@1596
   152
        }
edouard@1596
   153
vb@1409
   154
        state Grouped end=1 {
vb@563
   155
            on KeyGen
edouard@1281
   156
                do sendGroupUpdate;
edouard@1586
   157
            on CannotDecrypt {
edouard@1523
   158
                do sendUpdateRequest;
edouard@1586
   159
                do sendBeacon;
edouard@1586
   160
            }
edouard@1297
   161
            on UpdateRequest
edouard@1297
   162
                do sendGroupUpdate;
edouard@1523
   163
            on Beacon(Identity partner){
edouard@1216
   164
                do sendHandshakeRequest(partner);
edouard@1523
   165
                go GroupedBeaconed(partner);
edouard@1523
   166
            }
Edouard@594
   167
            on HandshakeRequest(Identity partner) {
vb@582
   168
                do sendHandshakeRequest(partner);
edouard@1216
   169
                go HandshakingGrouped(partner);
edouard@1216
   170
            }
edouard@1596
   171
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1586
   172
                do storeGroupUpdate(partner, keys);
edouard@1216
   173
        }
edouard@1216
   174
edouard@1523
   175
        state GroupedBeaconed timeout=600 (Identity expected){
edouard@1523
   176
            on KeyGen
edouard@1523
   177
                do sendGroupUpdate;
edouard@1586
   178
            on CannotDecrypt {
edouard@1523
   179
                do sendUpdateRequest;
edouard@1586
   180
                do sendBeacon;
edouard@1586
   181
            }
edouard@1523
   182
            on UpdateRequest
edouard@1523
   183
                do sendGroupUpdate;
edouard@1523
   184
            on Beacon(Identity partner){
edouard@1523
   185
                do sendHandshakeRequest(partner);
edouard@1523
   186
                go GroupedBeaconed(partner);
edouard@1523
   187
            }
edouard@1523
   188
            on HandshakeRequest(Identity partner) {
edouard@1523
   189
                if sameIdentities(partner, expected) {
edouard@1523
   190
                    // do nothing, to avoid sending handshake request twice 
edouard@1523
   191
                } else {
edouard@1523
   192
                    do sendHandshakeRequest(partner);
edouard@1523
   193
                }
edouard@1523
   194
                go HandshakingGrouped(partner);
edouard@1523
   195
            }
edouard@1596
   196
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1588
   197
                do storeGroupUpdate(partner, keys);
edouard@1523
   198
            on Timeout go Grouped;
edouard@1523
   199
        }
edouard@1523
   200
edouard@1460
   201
        state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1586
   202
            // HandshakeRequest from same group are filtered in receive_sync_msg
edouard@1586
   203
            on Init{
edouard@1586
   204
                if keyElectionWon(partner) {
edouard@1586
   205
                    do notifyInitAddOtherDevice(partner);
edouard@1586
   206
                } else {
edouard@1586
   207
                    do notifyInitMoveOurDevice(partner);
edouard@1586
   208
                }
edouard@1586
   209
            }
edouard@1216
   210
            on HandshakeRejected(Identity partner) {
edouard@1216
   211
                do rejectHandshake(partner);             // stores rejection of partner
edouard@1626
   212
                do sendGroupUpdate;
edouard@1216
   213
                go Grouped;
vb@563
   214
            }
edouard@1216
   215
            on HandshakeAccepted(Identity partner) {
edouard@1161
   216
                do acceptHandshake(partner); 
edouard@1626
   217
                do sendGroupUpdate;
edouard@1586
   218
                if keyElectionWon(partner) {
edouard@1586
   219
                    do sendGroupKeys(partner);
edouard@1586
   220
                    do notifyAcceptedDeviceAdded(partner);
edouard@1586
   221
                    go Grouped;
edouard@1586
   222
                }
edouard@1586
   223
                go WaitForGroupKeysGrouped(partner);
edouard@1586
   224
            }
edouard@1586
   225
            on Cancel go Grouped;
edouard@1597
   226
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1596
   227
                if sameIdentities(partner, expected) {
edouard@1597
   228
                    go WaitForAcceptGrouped(partner, groupkeys);
edouard@1596
   229
                }
edouard@1596
   230
            }
edouard@1626
   231
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   232
                do notifyOvertaken(partner);
edouard@1626
   233
                do storeGroupUpdate(partner, keys);
edouard@1626
   234
                go Grouped;
edouard@1626
   235
            }
edouard@1586
   236
            on Timeout {
edouard@1586
   237
                do notifyTimeout(expected);
edouard@1445
   238
                go Grouped;
edouard@1445
   239
            }
edouard@1586
   240
        }
edouard@1586
   241
edouard@1586
   242
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1597
   243
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1586
   244
                if sameIdentities(partner, expected) {
edouard@1597
   245
                    do storeGroupKeys(partner, groupkeys);
edouard@1586
   246
                    do sendGroupUpdate;
edouard@1601
   247
                    do renewUUID;
edouard@1586
   248
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   249
                    go Grouped;
edouard@1586
   250
                }
edouard@1586
   251
            }
edouard@1626
   252
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   253
                do notifyOvertaken(partner);
edouard@1626
   254
                do storeGroupUpdate(partner, keys);
edouard@1626
   255
                go Grouped;
edouard@1626
   256
            }
edouard@1445
   257
            on Timeout {
edouard@1477
   258
                do notifyTimeout(expected);
edouard@1216
   259
                go Grouped;
edouard@1161
   260
            }
vb@563
   261
        }
Edouard@613
   262
edouard@1597
   263
        state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   264
            on HandshakeRejected(Identity partner) {
edouard@1596
   265
                do rejectHandshake(partner);
edouard@1626
   266
                do sendGroupUpdate;
edouard@1596
   267
                go Grouped;
edouard@1596
   268
            }
edouard@1596
   269
            on HandshakeAccepted(Identity partner) {
edouard@1647
   270
                if sameIdentities(partner, expected) {
edouard@1647
   271
                    do acceptHandshake(partner); 
edouard@1647
   272
                    do storeGroupKeys(partner, groupkeys);
edouard@1647
   273
                    do sendGroupUpdate;
edouard@1647
   274
                    do renewUUID;
edouard@1647
   275
                    do notifyAcceptedDeviceMoved(partner);
edouard@1647
   276
                }
edouard@1596
   277
                go Grouped;
edouard@1596
   278
            }
edouard@1596
   279
            on Cancel go Grouped;
edouard@1626
   280
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   281
                do notifyOvertaken(partner);
edouard@1626
   282
                do storeGroupUpdate(partner, keys);
edouard@1626
   283
                go Grouped;
edouard@1626
   284
            }
edouard@1596
   285
            on Timeout {
edouard@1596
   286
                do notifyTimeout(expected);
edouard@1596
   287
                go Grouped;
edouard@1596
   288
            }
edouard@1596
   289
        }
edouard@1596
   290
vb@951
   291
        tag Init 1;
vb@951
   292
        tag Beacon 2;
vb@951
   293
        tag HandshakeRequest 3;
vb@951
   294
        tag GroupKeys 4;
Edouard@613
   295
    }
vb@563
   296
}
vb@563
   297