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