sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Tue, 07 Mar 2017 15:49:15 +0100
branchAllGroupDevicesShowHandshake
changeset 1626 22343c95398a
parent 1601 10e4e77e2278
child 1647 f089d9e32e60
permissions -rw-r--r--
KeySync: modified FSM to have Sync Handshake Dialog to be displayed on each device of the same group, and disapear when handshake is over.
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@1596
   145
            }
edouard@1596
   146
            on Cancel go Sole;
edouard@1596
   147
            on Timeout {
edouard@1596
   148
                do notifyTimeout(expected);
edouard@1596
   149
                go Sole;
edouard@1596
   150
            }
edouard@1596
   151
        }
edouard@1596
   152
vb@1409
   153
        state Grouped end=1 {
vb@563
   154
            on KeyGen
edouard@1281
   155
                do sendGroupUpdate;
edouard@1586
   156
            on CannotDecrypt {
edouard@1523
   157
                do sendUpdateRequest;
edouard@1586
   158
                do sendBeacon;
edouard@1586
   159
            }
edouard@1297
   160
            on UpdateRequest
edouard@1297
   161
                do sendGroupUpdate;
edouard@1523
   162
            on Beacon(Identity partner){
edouard@1216
   163
                do sendHandshakeRequest(partner);
edouard@1523
   164
                go GroupedBeaconed(partner);
edouard@1523
   165
            }
Edouard@594
   166
            on HandshakeRequest(Identity partner) {
vb@582
   167
                do sendHandshakeRequest(partner);
edouard@1216
   168
                go HandshakingGrouped(partner);
edouard@1216
   169
            }
edouard@1596
   170
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1586
   171
                do storeGroupUpdate(partner, keys);
edouard@1216
   172
        }
edouard@1216
   173
edouard@1523
   174
        state GroupedBeaconed timeout=600 (Identity expected){
edouard@1523
   175
            on KeyGen
edouard@1523
   176
                do sendGroupUpdate;
edouard@1586
   177
            on CannotDecrypt {
edouard@1523
   178
                do sendUpdateRequest;
edouard@1586
   179
                do sendBeacon;
edouard@1586
   180
            }
edouard@1523
   181
            on UpdateRequest
edouard@1523
   182
                do sendGroupUpdate;
edouard@1523
   183
            on Beacon(Identity partner){
edouard@1523
   184
                do sendHandshakeRequest(partner);
edouard@1523
   185
                go GroupedBeaconed(partner);
edouard@1523
   186
            }
edouard@1523
   187
            on HandshakeRequest(Identity partner) {
edouard@1523
   188
                if sameIdentities(partner, expected) {
edouard@1523
   189
                    // do nothing, to avoid sending handshake request twice 
edouard@1523
   190
                } else {
edouard@1523
   191
                    do sendHandshakeRequest(partner);
edouard@1523
   192
                }
edouard@1523
   193
                go HandshakingGrouped(partner);
edouard@1523
   194
            }
edouard@1596
   195
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1588
   196
                do storeGroupUpdate(partner, keys);
edouard@1523
   197
            on Timeout go Grouped;
edouard@1523
   198
        }
edouard@1523
   199
edouard@1460
   200
        state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1586
   201
            // HandshakeRequest from same group are filtered in receive_sync_msg
edouard@1586
   202
            on Init{
edouard@1586
   203
                if keyElectionWon(partner) {
edouard@1586
   204
                    do notifyInitAddOtherDevice(partner);
edouard@1586
   205
                } else {
edouard@1586
   206
                    do notifyInitMoveOurDevice(partner);
edouard@1586
   207
                }
edouard@1586
   208
            }
edouard@1216
   209
            on HandshakeRejected(Identity partner) {
edouard@1216
   210
                do rejectHandshake(partner);             // stores rejection of partner
edouard@1626
   211
                do sendGroupUpdate;
edouard@1216
   212
                go Grouped;
vb@563
   213
            }
edouard@1216
   214
            on HandshakeAccepted(Identity partner) {
edouard@1161
   215
                do acceptHandshake(partner); 
edouard@1626
   216
                do sendGroupUpdate;
edouard@1586
   217
                if keyElectionWon(partner) {
edouard@1586
   218
                    do sendGroupKeys(partner);
edouard@1586
   219
                    do notifyAcceptedDeviceAdded(partner);
edouard@1586
   220
                    go Grouped;
edouard@1586
   221
                }
edouard@1586
   222
                go WaitForGroupKeysGrouped(partner);
edouard@1586
   223
            }
edouard@1586
   224
            on Cancel go Grouped;
edouard@1597
   225
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1596
   226
                if sameIdentities(partner, expected) {
edouard@1597
   227
                    go WaitForAcceptGrouped(partner, groupkeys);
edouard@1596
   228
                }
edouard@1596
   229
            }
edouard@1626
   230
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   231
                do notifyOvertaken(partner);
edouard@1626
   232
                do storeGroupUpdate(partner, keys);
edouard@1626
   233
                go Grouped;
edouard@1626
   234
            }
edouard@1586
   235
            on Timeout {
edouard@1586
   236
                do notifyTimeout(expected);
edouard@1445
   237
                go Grouped;
edouard@1445
   238
            }
edouard@1586
   239
        }
edouard@1586
   240
edouard@1586
   241
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1597
   242
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1586
   243
                if sameIdentities(partner, expected) {
edouard@1597
   244
                    do storeGroupKeys(partner, groupkeys);
edouard@1586
   245
                    do sendGroupUpdate;
edouard@1601
   246
                    do renewUUID;
edouard@1586
   247
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   248
                    go Grouped;
edouard@1586
   249
                }
edouard@1586
   250
            }
edouard@1626
   251
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   252
                do notifyOvertaken(partner);
edouard@1626
   253
                do storeGroupUpdate(partner, keys);
edouard@1626
   254
                go Grouped;
edouard@1626
   255
            }
edouard@1445
   256
            on Timeout {
edouard@1477
   257
                do notifyTimeout(expected);
edouard@1216
   258
                go Grouped;
edouard@1161
   259
            }
vb@563
   260
        }
Edouard@613
   261
edouard@1597
   262
        state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   263
            on HandshakeRejected(Identity partner) {
edouard@1596
   264
                do rejectHandshake(partner);
edouard@1626
   265
                do sendGroupUpdate;
edouard@1596
   266
                go Grouped;
edouard@1596
   267
            }
edouard@1596
   268
            on HandshakeAccepted(Identity partner) {
edouard@1596
   269
                do acceptHandshake(partner); 
edouard@1597
   270
                do storeGroupKeys(partner, groupkeys);
edouard@1596
   271
                do sendGroupUpdate;
edouard@1601
   272
                do renewUUID;
edouard@1596
   273
                do notifyAcceptedDeviceMoved(partner);
edouard@1596
   274
                go Grouped;
edouard@1596
   275
            }
edouard@1596
   276
            on Cancel go Grouped;
edouard@1626
   277
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   278
                do notifyOvertaken(partner);
edouard@1626
   279
                do storeGroupUpdate(partner, keys);
edouard@1626
   280
                go Grouped;
edouard@1626
   281
            }
edouard@1596
   282
            on Timeout {
edouard@1596
   283
                do notifyTimeout(expected);
edouard@1596
   284
                go Grouped;
edouard@1596
   285
            }
edouard@1596
   286
        }
edouard@1596
   287
vb@951
   288
        tag Init 1;
vb@951
   289
        tag Beacon 2;
vb@951
   290
        tag HandshakeRequest 3;
vb@951
   291
        tag GroupKeys 4;
Edouard@613
   292
    }
vb@563
   293
}
vb@563
   294