sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Wed, 19 Apr 2017 18:31:57 +0200
changeset 1724 a2a8ffce4a01
parent 1723 c93e1ddf1059
child 1727 7a905529fc0e
permissions -rw-r--r--
Sync : fixed some wrong sementics in FSM, and added missing check. Doesn't fix any known bug.
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@1724
    74
                if keyElectionWon(expected) {
edouard@1724
    75
                    do notifyInitFormGroup(expected);
edouard@1477
    76
                } else {
edouard@1724
    77
                    do notifyInitAddOurDevice(expected);
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@1724
   100
                if keyElectionWon(expected) {
edouard@1724
   101
                    // not supposed 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@1724
   207
                if keyElectionWon(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@1724
   230
                if keyElectionWon(expected) {
edouard@1724
   231
                    // not supposed to receive groupkeys - ignore
edouard@1724
   232
                } else {
edouard@1724
   233
                    // UUID changes in between, so we can only check for same address and fpr
edouard@1724
   234
                    if sameKeyAndAddress(partner, expected) {
edouard@1724
   235
                        go WaitForAcceptGrouped(partner, groupkeys);
edouard@1724
   236
                    }
edouard@1596
   237
                }
edouard@1596
   238
            }
edouard@1626
   239
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   240
                do notifyOvertaken(partner);
edouard@1626
   241
                do storeGroupUpdate(partner, keys);
edouard@1626
   242
                go Grouped;
edouard@1626
   243
            }
edouard@1586
   244
            on Timeout {
edouard@1586
   245
                do notifyTimeout(expected);
edouard@1445
   246
                go Grouped;
edouard@1445
   247
            }
edouard@1586
   248
        }
edouard@1586
   249
edouard@1586
   250
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1597
   251
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1586
   252
                if sameIdentities(partner, expected) {
edouard@1597
   253
                    do storeGroupKeys(partner, groupkeys);
edouard@1586
   254
                    do sendGroupUpdate;
edouard@1601
   255
                    do renewUUID;
edouard@1586
   256
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   257
                    go Grouped;
edouard@1586
   258
                }
edouard@1586
   259
            }
edouard@1626
   260
            on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1626
   261
                do notifyOvertaken(partner);
edouard@1626
   262
                do storeGroupUpdate(partner, keys);
edouard@1626
   263
                go Grouped;
edouard@1626
   264
            }
edouard@1445
   265
            on Timeout {
edouard@1477
   266
                do notifyTimeout(expected);
edouard@1216
   267
                go Grouped;
edouard@1161
   268
            }
vb@563
   269
        }
Edouard@613
   270
edouard@1597
   271
        state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   272
            on HandshakeRejected(Identity partner) {
edouard@1596
   273
                do rejectHandshake(partner);
edouard@1626
   274
                do sendGroupUpdate;
edouard@1596
   275
                go Grouped;
edouard@1596
   276
            }
edouard@1596
   277
            on HandshakeAccepted(Identity partner) {
edouard@1647
   278
                if sameIdentities(partner, expected) {
edouard@1647
   279
                    do acceptHandshake(partner); 
edouard@1647
   280
                    do storeGroupKeys(partner, groupkeys);
edouard@1647
   281
                    do sendGroupUpdate;
edouard@1647
   282
                    do renewUUID;
edouard@1647
   283
                    do notifyAcceptedDeviceMoved(partner);
edouard@1647
   284
                }
edouard@1596
   285
                go Grouped;
edouard@1596
   286
            }
edouard@1596
   287
            on Cancel go Grouped;
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@1596
   293
            on Timeout {
edouard@1596
   294
                do notifyTimeout(expected);
edouard@1596
   295
                go Grouped;
edouard@1596
   296
            }
edouard@1596
   297
        }
edouard@1596
   298
vb@951
   299
        tag Init 1;
vb@951
   300
        tag Beacon 2;
vb@951
   301
        tag HandshakeRequest 3;
vb@951
   302
        tag GroupKeys 4;
Edouard@613
   303
    }
vb@563
   304
}
vb@563
   305