sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Tue, 21 Feb 2017 23:08:01 +0100
changeset 1601 10e4e77e2278
parent 1597 cc039a6139cb
child 1626 22343c95398a
permissions -rw-r--r--
KeySync : made UUID renewal when entering group explicit in fsm, and moved it after sendGroupKeys to be sure it is accepted by peer. Also fixed bug generating else part of conditions in fsm.
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@1216
   211
                go Grouped;
vb@563
   212
            }
edouard@1216
   213
            on HandshakeAccepted(Identity partner) {
edouard@1161
   214
                do acceptHandshake(partner); 
edouard@1586
   215
                if keyElectionWon(partner) {
edouard@1586
   216
                    do sendGroupKeys(partner);
edouard@1586
   217
                    do notifyAcceptedDeviceAdded(partner);
edouard@1586
   218
                    go Grouped;
edouard@1586
   219
                }
edouard@1586
   220
                go WaitForGroupKeysGrouped(partner);
edouard@1586
   221
            }
edouard@1586
   222
            on Cancel go Grouped;
edouard@1597
   223
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1596
   224
                if sameIdentities(partner, expected) {
edouard@1597
   225
                    go WaitForAcceptGrouped(partner, groupkeys);
edouard@1596
   226
                }
edouard@1596
   227
            }
edouard@1586
   228
            on Timeout {
edouard@1586
   229
                do notifyTimeout(expected);
edouard@1445
   230
                go Grouped;
edouard@1445
   231
            }
edouard@1586
   232
        }
edouard@1586
   233
edouard@1586
   234
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1597
   235
            on GroupKeys(Identity partner, GroupKeys groupkeys) {
edouard@1586
   236
                if sameIdentities(partner, expected) {
edouard@1597
   237
                    do storeGroupKeys(partner, groupkeys);
edouard@1586
   238
                    do sendGroupUpdate;
edouard@1601
   239
                    do renewUUID;
edouard@1586
   240
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   241
                    go Grouped;
edouard@1586
   242
                }
edouard@1586
   243
            }
edouard@1445
   244
            on Timeout {
edouard@1477
   245
                do notifyTimeout(expected);
edouard@1216
   246
                go Grouped;
edouard@1161
   247
            }
vb@563
   248
        }
Edouard@613
   249
edouard@1597
   250
        state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
edouard@1596
   251
            on HandshakeRejected(Identity partner) {
edouard@1596
   252
                do rejectHandshake(partner);
edouard@1596
   253
                go Grouped;
edouard@1596
   254
            }
edouard@1596
   255
            on HandshakeAccepted(Identity partner) {
edouard@1596
   256
                do acceptHandshake(partner); 
edouard@1597
   257
                do storeGroupKeys(partner, groupkeys);
edouard@1596
   258
                do sendGroupUpdate;
edouard@1601
   259
                do renewUUID;
edouard@1596
   260
                do notifyAcceptedDeviceMoved(partner);
edouard@1596
   261
                go Grouped;
edouard@1596
   262
            }
edouard@1596
   263
            on Cancel go Grouped;
edouard@1596
   264
            on Timeout {
edouard@1596
   265
                do notifyTimeout(expected);
edouard@1596
   266
                go Grouped;
edouard@1596
   267
            }
edouard@1596
   268
        }
edouard@1596
   269
vb@951
   270
        tag Init 1;
vb@951
   271
        tag Beacon 2;
vb@951
   272
        tag HandshakeRequest 3;
vb@951
   273
        tag GroupKeys 4;
Edouard@613
   274
    }
vb@563
   275
}
vb@563
   276