sync/devicegroup.fsm
author Krista Bennett <krista@pep-project.org>
Thu, 26 Oct 2017 15:56:01 +0200
branchtest_diphoton
changeset 2208 b19261f4fed4
parent 1749 32084f52dada
permissions -rw-r--r--
merged in default
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@1749
   187
edouard@1749
   188
                ///// de-activate 3+ de group in test_diphoton
edouard@1749
   189
                // do sendBeacon;
edouard@1749
   190
edouard@1739
   191
                go GroupWaiting;
edouard@1586
   192
            }
edouard@1297
   193
            on UpdateRequest
edouard@1297
   194
                do sendGroupUpdate;
edouard@1749
   195
edouard@1749
   196
            ///// de-activate 3+ de group in test_diphoton
edouard@1749
   197
            // on Beacon(Identity partner){
edouard@1749
   198
            //     do sendHandshakeRequest(partner);
edouard@1749
   199
            //     go GroupedBeaconed(partner);
edouard@1749
   200
            // }
edouard@1749
   201
            // on HandshakeRequest(Identity partner) {
edouard@1749
   202
            //     do sendHandshakeRequest(partner);
edouard@1749
   203
            //     go HandshakingGrouped(partner);
edouard@1749
   204
            // }
edouard@1749
   205
edouard@1596
   206
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1586
   207
                do storeGroupUpdate(partner, keys);
edouard@1216
   208
        }
edouard@1216
   209
edouard@1739
   210
        // copy of grouped state, with a timeout to enable fast poling for a minut
edouard@1739
   211
        state GroupWaiting timeout=60 {
edouard@1739
   212
            on KeyGen
edouard@1739
   213
                do sendGroupUpdate;
edouard@1739
   214
            on CannotDecrypt {
edouard@1739
   215
                do sendUpdateRequest;
edouard@1749
   216
edouard@1749
   217
                ///// de-activate 3+ de group in test_diphoton
edouard@1749
   218
                // do sendBeacon;
edouard@1739
   219
            }
edouard@1739
   220
            on UpdateRequest
edouard@1739
   221
                do sendGroupUpdate;
edouard@1749
   222
edouard@1749
   223
            ///// de-activate 3+ de group in test_diphoton
edouard@1749
   224
            // on Beacon(Identity partner){
edouard@1749
   225
            //     do sendHandshakeRequest(partner);
edouard@1749
   226
            //     go GroupedBeaconed(partner);
edouard@1749
   227
            // }
edouard@1749
   228
            // on HandshakeRequest(Identity partner) {
edouard@1749
   229
            //     do sendHandshakeRequest(partner);
edouard@1749
   230
            //     go HandshakingGrouped(partner);
edouard@1749
   231
            // }
edouard@1749
   232
edouard@1739
   233
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1739
   234
                do storeGroupUpdate(partner, keys);
edouard@1739
   235
            on Timeout go Grouped;
edouard@1739
   236
        }
edouard@1739
   237
edouard@1749
   238
        ///// de-activate 3+ de group in test_diphoton
edouard@1749
   239
        // state GroupedBeaconed timeout=600 (Identity expected){
edouard@1749
   240
        //     on KeyGen
edouard@1749
   241
        //         do sendGroupUpdate;
edouard@1749
   242
        //     on CannotDecrypt {
edouard@1749
   243
        //         do sendUpdateRequest;
edouard@1749
   244
        //         do sendBeacon;
edouard@1749
   245
        //     }
edouard@1749
   246
        //     on UpdateRequest
edouard@1749
   247
        //         do sendGroupUpdate;
edouard@1749
   248
        //     on Beacon(Identity partner){
edouard@1749
   249
        //         do sendHandshakeRequest(partner);
edouard@1749
   250
        //         go GroupedBeaconed(partner);
edouard@1749
   251
        //     }
edouard@1749
   252
        //     on HandshakeRequest(Identity partner) {
edouard@1749
   253
        //         if sameIdentities(partner, expected) {
edouard@1749
   254
        //             // do nothing, to avoid sending handshake request twice 
edouard@1749
   255
        //         } else {
edouard@1749
   256
        //             do sendHandshakeRequest(partner);
edouard@1749
   257
        //         }
edouard@1749
   258
        //         go HandshakingGrouped(partner);
edouard@1749
   259
        //     }
edouard@1749
   260
        //     on GroupUpdate(Identity partner, IdentityList keys)
edouard@1749
   261
        //         do storeGroupUpdate(partner, keys);
edouard@1749
   262
        //     on Timeout go Grouped;
edouard@1749
   263
        // }
edouard@1523
   264
edouard@1749
   265
        ///// de-activate 3+ de group in test_diphoton
edouard@1749
   266
        // state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1749
   267
        //     // HandshakeRequest from same group are filtered in receive_sync_msg
edouard@1749
   268
        //     on Init{
edouard@1749
   269
        //         if keyElectionWon(expected) {
edouard@1749
   270
        //             do notifyInitAddOtherDevice(partner);
edouard@1749
   271
        //         } else {
edouard@1749
   272
        //             do notifyInitMoveOurDevice(partner);
edouard@1749
   273
        //         }
edouard@1749
   274
        //     }
edouard@1749
   275
        //     on HandshakeRejected(Identity partner) {
edouard@1749
   276
        //         do rejectHandshake(partner);             // stores rejection of partner
edouard@1749
   277
        //         do sendGroupUpdate;
edouard@1749
   278
        //         go Grouped;
edouard@1749
   279
        //     }
edouard@1749
   280
        //     on HandshakeAccepted(Identity partner) {
edouard@1749
   281
        //         do acceptHandshake(partner); 
edouard@1749
   282
        //         do sendGroupUpdate;
edouard@1749
   283
        //         if keyElectionWon(partner) {
edouard@1749
   284
        //             do sendGroupKeys(partner);
edouard@1749
   285
        //             do notifyAcceptedDeviceAdded(partner);
edouard@1749
   286
        //             go Grouped;
edouard@1749
   287
        //         }
edouard@1749
   288
        //         go WaitForGroupKeysGrouped(partner);
edouard@1749
   289
        //     }
edouard@1749
   290
        //     on Cancel go Grouped;
edouard@1749
   291
        //     on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1749
   292
        //         if keyElectionWon(expected) {
edouard@1749
   293
        //             // not supposed to receive groupkeys - ignore
edouard@1749
   294
        //         } else {
edouard@1749
   295
        //             // UUID changes in between, so we can only check for same address and fpr
edouard@1749
   296
        //             if sameKeyAndAddress(partner, expected) {
edouard@1749
   297
        //                 go WaitForAcceptGrouped(partner, groupkeys);
edouard@1749
   298
        //             }
edouard@1749
   299
        //         }
edouard@1749
   300
        //     }
edouard@1749
   301
        //     on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1749
   302
        //         do notifyOvertaken(partner);
edouard@1749
   303
        //         do storeGroupUpdate(partner, keys);
edouard@1749
   304
        //         go Grouped;
edouard@1749
   305
        //     }
edouard@1749
   306
        //     on Timeout {
edouard@1749
   307
        //         do notifyTimeout(expected);
edouard@1749
   308
        //         go Grouped;
edouard@1749
   309
        //     }
edouard@1749
   310
        // }
edouard@1586
   311
edouard@1749
   312
        ///// de-activate 3+ de group in test_diphoton
edouard@1749
   313
        // state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1749
   314
        //     on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1749
   315
        //         if sameIdentities(partner, expected) {
edouard@1749
   316
        //             do storeGroupKeys(partner, groupkeys);
edouard@1749
   317
        //             do sendGroupUpdate;
edouard@1749
   318
        //             do renewUUID;
edouard@1749
   319
        //             do notifyAcceptedDeviceMoved(partner);
edouard@1749
   320
        //             go Grouped;
edouard@1749
   321
        //         }
edouard@1749
   322
        //     }
edouard@1749
   323
        //     on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1749
   324
        //         do notifyOvertaken(partner);
edouard@1749
   325
        //         do storeGroupUpdate(partner, keys);
edouard@1749
   326
        //         go Grouped;
edouard@1749
   327
        //     }
edouard@1749
   328
        //     on Timeout {
edouard@1749
   329
        //         do notifyTimeout(expected);
edouard@1749
   330
        //         go Grouped;
edouard@1749
   331
        //     }
edouard@1749
   332
        // }
Edouard@613
   333
edouard@1749
   334
        ///// de-activate 3+ de group in test_diphoton
edouard@1749
   335
        // state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1749
   336
        //     on HandshakeRejected(Identity partner) {
edouard@1749
   337
        //         do rejectHandshake(partner);
edouard@1749
   338
        //         do sendGroupUpdate;
edouard@1749
   339
        //         go Grouped;
edouard@1749
   340
        //     }
edouard@1749
   341
        //     on HandshakeAccepted(Identity partner) {
edouard@1749
   342
        //         if sameIdentities(partner, expected) {
edouard@1749
   343
        //             do acceptHandshake(partner); 
edouard@1749
   344
        //             do storeGroupKeys(partner, groupkeys);
edouard@1749
   345
        //             do sendGroupUpdate;
edouard@1749
   346
        //             do renewUUID;
edouard@1749
   347
        //             do notifyAcceptedDeviceMoved(partner);
edouard@1749
   348
        //         }
edouard@1749
   349
        //         go Grouped;
edouard@1749
   350
        //     }
edouard@1749
   351
        //     on Cancel go Grouped;
edouard@1749
   352
        //     on GroupUpdate(Identity partner, IdentityList keys) {
edouard@1749
   353
        //         do notifyOvertaken(partner);
edouard@1749
   354
        //         do storeGroupUpdate(partner, keys);
edouard@1749
   355
        //         go Grouped;
edouard@1749
   356
        //     }
edouard@1749
   357
        //     on Timeout {
edouard@1749
   358
        //         do notifyTimeout(expected);
edouard@1749
   359
        //         go Grouped;
edouard@1749
   360
        //     }
edouard@1749
   361
        // }
edouard@1596
   362
vb@951
   363
        tag Init 1;
vb@951
   364
        tag Beacon 2;
vb@951
   365
        tag HandshakeRequest 3;
vb@951
   366
        tag GroupKeys 4;
Edouard@613
   367
    }
vb@563
   368
}
vb@563
   369