sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Mon, 20 Feb 2017 14:10:36 +0100
branchKeySyncWaitForAccept
changeset 1596 f7c8b7401911
parent 1590 6e007351ccde
child 1597 cc039a6139cb
permissions -rw-r--r--
KeySync : added WaitForAccept(Sole|Grouped) states to deal with GroupKeys received before Handshake is accepted on device losing key election.
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@1588
    90
                        do notifyAcceptedGroupCreated(partner);
edouard@1588
    91
                        go Grouped;
edouard@1588
    92
                    }
edouard@1588
    93
                    go WaitForGroupKeysSole(partner);
vb@563
    94
                }
edouard@1588
    95
                go Sole;
vb@563
    96
            }
edouard@1445
    97
            on Cancel go Sole;
edouard@1596
    98
            on GroupKeys(Identity partner, IdentityList keys) {
edouard@1596
    99
                if sameIdentities(partner, expected) {
edouard@1596
   100
                    go WaitForAcceptSole(partner, keys);
edouard@1596
   101
                }
edouard@1596
   102
            }
edouard@1445
   103
            on Timeout {
edouard@1477
   104
                do notifyTimeout(expected);
edouard@1555
   105
                do sendBeacon;
edouard@1445
   106
                go Sole;
edouard@1445
   107
            }
vb@563
   108
        }
vb@563
   109
    
edouard@1460
   110
        state WaitForGroupKeysSole timeout=600 (Identity expected) {
edouard@1596
   111
            on GroupKeys(Identity partner, IdentityList keys) {
edouard@1523
   112
                if sameIdentities(partner, expected) {
edouard@1523
   113
                    do storeGroupKeys(partner, keys);
edouard@1566
   114
                    do sendGroupUpdate;
edouard@1523
   115
                    do notifyAcceptedDeviceAdded(partner);
edouard@1523
   116
                    go Grouped;
edouard@1523
   117
                }
vb@563
   118
            }
edouard@1445
   119
            on Timeout {
edouard@1477
   120
                do notifyTimeout(expected);
vb@569
   121
                go Sole;
vb@569
   122
            }
vb@563
   123
        }
vb@563
   124
edouard@1596
   125
        state WaitForAcceptSole timeout=600 (Identity expected, IdentityList keys) {
edouard@1596
   126
            on HandshakeRejected(Identity partner) {
edouard@1596
   127
                do rejectHandshake(partner);
edouard@1596
   128
                go Sole;
edouard@1596
   129
            }
edouard@1596
   130
            on HandshakeAccepted(Identity partner) {
edouard@1596
   131
                if sameIdentities(partner, expected) {
edouard@1596
   132
                    do acceptHandshake(partner); 
edouard@1596
   133
                    do storeGroupKeys(partner, keys);
edouard@1596
   134
                    do sendGroupUpdate;
edouard@1596
   135
                    do notifyAcceptedDeviceAdded(partner);
edouard@1596
   136
                    go Grouped;
edouard@1596
   137
                }
edouard@1596
   138
                go Sole;
edouard@1596
   139
            }
edouard@1596
   140
            on Cancel go Sole;
edouard@1596
   141
            on Timeout {
edouard@1596
   142
                do notifyTimeout(expected);
edouard@1596
   143
                go Sole;
edouard@1596
   144
            }
edouard@1596
   145
        }
edouard@1596
   146
vb@1409
   147
        state Grouped end=1 {
vb@563
   148
            on KeyGen
edouard@1281
   149
                do sendGroupUpdate;
edouard@1586
   150
            on CannotDecrypt {
edouard@1523
   151
                do sendUpdateRequest;
edouard@1586
   152
                do sendBeacon;
edouard@1586
   153
            }
edouard@1297
   154
            on UpdateRequest
edouard@1297
   155
                do sendGroupUpdate;
edouard@1523
   156
            on Beacon(Identity partner){
edouard@1216
   157
                do sendHandshakeRequest(partner);
edouard@1523
   158
                go GroupedBeaconed(partner);
edouard@1523
   159
            }
Edouard@594
   160
            on HandshakeRequest(Identity partner) {
vb@582
   161
                do sendHandshakeRequest(partner);
edouard@1216
   162
                go HandshakingGrouped(partner);
edouard@1216
   163
            }
edouard@1596
   164
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1586
   165
                do storeGroupUpdate(partner, keys);
edouard@1216
   166
        }
edouard@1216
   167
edouard@1523
   168
        state GroupedBeaconed timeout=600 (Identity expected){
edouard@1523
   169
            on KeyGen
edouard@1523
   170
                do sendGroupUpdate;
edouard@1586
   171
            on CannotDecrypt {
edouard@1523
   172
                do sendUpdateRequest;
edouard@1586
   173
                do sendBeacon;
edouard@1586
   174
            }
edouard@1523
   175
            on UpdateRequest
edouard@1523
   176
                do sendGroupUpdate;
edouard@1523
   177
            on Beacon(Identity partner){
edouard@1523
   178
                do sendHandshakeRequest(partner);
edouard@1523
   179
                go GroupedBeaconed(partner);
edouard@1523
   180
            }
edouard@1523
   181
            on HandshakeRequest(Identity partner) {
edouard@1523
   182
                if sameIdentities(partner, expected) {
edouard@1523
   183
                    // do nothing, to avoid sending handshake request twice 
edouard@1523
   184
                } else {
edouard@1523
   185
                    do sendHandshakeRequest(partner);
edouard@1523
   186
                }
edouard@1523
   187
                go HandshakingGrouped(partner);
edouard@1523
   188
            }
edouard@1596
   189
            on GroupUpdate(Identity partner, IdentityList keys)
edouard@1588
   190
                do storeGroupUpdate(partner, keys);
edouard@1523
   191
            on Timeout go Grouped;
edouard@1523
   192
        }
edouard@1523
   193
edouard@1460
   194
        state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1586
   195
            // HandshakeRequest from same group are filtered in receive_sync_msg
edouard@1586
   196
            on Init{
edouard@1586
   197
                if keyElectionWon(partner) {
edouard@1586
   198
                    do notifyInitAddOtherDevice(partner);
edouard@1586
   199
                } else {
edouard@1586
   200
                    do notifyInitMoveOurDevice(partner);
edouard@1586
   201
                }
edouard@1586
   202
            }
edouard@1216
   203
            on HandshakeRejected(Identity partner) {
edouard@1216
   204
                do rejectHandshake(partner);             // stores rejection of partner
edouard@1216
   205
                go Grouped;
vb@563
   206
            }
edouard@1216
   207
            on HandshakeAccepted(Identity partner) {
edouard@1161
   208
                do acceptHandshake(partner); 
edouard@1586
   209
                if keyElectionWon(partner) {
edouard@1586
   210
                    do sendGroupKeys(partner);
edouard@1586
   211
                    do notifyAcceptedDeviceAdded(partner);
edouard@1586
   212
                    go Grouped;
edouard@1586
   213
                }
edouard@1586
   214
                go WaitForGroupKeysGrouped(partner);
edouard@1586
   215
            }
edouard@1586
   216
            on Cancel go Grouped;
edouard@1596
   217
            on GroupKeys(Identity partner, IdentityList keys) {
edouard@1596
   218
                if sameIdentities(partner, expected) {
edouard@1596
   219
                    go WaitForAcceptGrouped(partner, keys);
edouard@1596
   220
                }
edouard@1596
   221
            }
edouard@1586
   222
            on Timeout {
edouard@1586
   223
                do notifyTimeout(expected);
edouard@1445
   224
                go Grouped;
edouard@1445
   225
            }
edouard@1586
   226
        }
edouard@1586
   227
edouard@1586
   228
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1596
   229
            on GroupKeys(Identity partner, IdentityList keys) {
edouard@1586
   230
                if sameIdentities(partner, expected) {
edouard@1586
   231
                    do storeGroupKeys(partner, keys);
edouard@1586
   232
                    do sendGroupUpdate;
edouard@1586
   233
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   234
                    go Grouped;
edouard@1586
   235
                }
edouard@1586
   236
            }
edouard@1445
   237
            on Timeout {
edouard@1477
   238
                do notifyTimeout(expected);
edouard@1216
   239
                go Grouped;
edouard@1161
   240
            }
vb@563
   241
        }
Edouard@613
   242
edouard@1596
   243
        state WaitForAcceptGrouped timeout=600 (Identity expected, IdentityList keys) {
edouard@1596
   244
            on HandshakeRejected(Identity partner) {
edouard@1596
   245
                do rejectHandshake(partner);
edouard@1596
   246
                go Grouped;
edouard@1596
   247
            }
edouard@1596
   248
            on HandshakeAccepted(Identity partner) {
edouard@1596
   249
                do acceptHandshake(partner); 
edouard@1596
   250
                do storeGroupKeys(partner, keys);
edouard@1596
   251
                do sendGroupUpdate;
edouard@1596
   252
                do notifyAcceptedDeviceMoved(partner);
edouard@1596
   253
                go Grouped;
edouard@1596
   254
            }
edouard@1596
   255
            on Cancel go Grouped;
edouard@1596
   256
            on Timeout {
edouard@1596
   257
                do notifyTimeout(expected);
edouard@1596
   258
                go Grouped;
edouard@1596
   259
            }
edouard@1596
   260
        }
edouard@1596
   261
vb@951
   262
        tag Init 1;
vb@951
   263
        tag Beacon 2;
vb@951
   264
        tag HandshakeRequest 3;
vb@951
   265
        tag GroupKeys 4;
Edouard@613
   266
    }
vb@563
   267
}
vb@563
   268