sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Sat, 18 Feb 2017 23:08:34 +0100
branchGroupMerge
changeset 1588 1a43a7eddf90
parent 1586 599deda50386
child 1590 6e007351ccde
permissions -rw-r--r--
KeySync fsm : fixed storeGroupKeys instead of storeGroupUpdate, added more check, fixed wrong parameter type for storeGroupKeys
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@1445
    98
            on Timeout {
edouard@1477
    99
                do notifyTimeout(expected);
edouard@1555
   100
                do sendBeacon;
edouard@1445
   101
                go Sole;
edouard@1445
   102
            }
vb@563
   103
        }
vb@563
   104
    
edouard@1460
   105
        state WaitForGroupKeysSole timeout=600 (Identity expected) {
edouard@1588
   106
            on GroupKeys(Identity partner, identity_list keys) {
edouard@1523
   107
                if sameIdentities(partner, expected) {
edouard@1523
   108
                    do storeGroupKeys(partner, keys);
edouard@1566
   109
                    do sendGroupUpdate;
edouard@1523
   110
                    do notifyAcceptedDeviceAdded(partner);
edouard@1523
   111
                    go Grouped;
edouard@1523
   112
                }
vb@563
   113
            }
edouard@1445
   114
            on Timeout {
edouard@1477
   115
                do notifyTimeout(expected);
vb@569
   116
                go Sole;
vb@569
   117
            }
vb@563
   118
        }
vb@563
   119
vb@1409
   120
        state Grouped end=1 {
vb@563
   121
            on KeyGen
edouard@1281
   122
                do sendGroupUpdate;
edouard@1586
   123
            on CannotDecrypt {
edouard@1523
   124
                do sendUpdateRequest;
edouard@1586
   125
                do sendBeacon;
edouard@1586
   126
            }
edouard@1297
   127
            on UpdateRequest
edouard@1297
   128
                do sendGroupUpdate;
edouard@1523
   129
            on Beacon(Identity partner){
edouard@1216
   130
                do sendHandshakeRequest(partner);
edouard@1523
   131
                go GroupedBeaconed(partner);
edouard@1523
   132
            }
Edouard@594
   133
            on HandshakeRequest(Identity partner) {
vb@582
   134
                do sendHandshakeRequest(partner);
edouard@1216
   135
                go HandshakingGrouped(partner);
edouard@1216
   136
            }
edouard@1588
   137
            on GroupUpdate(Identity partner, identity_list keys)
edouard@1586
   138
                do storeGroupUpdate(partner, keys);
edouard@1216
   139
        }
edouard@1216
   140
edouard@1523
   141
        state GroupedBeaconed timeout=600 (Identity expected){
edouard@1523
   142
            on KeyGen
edouard@1523
   143
                do sendGroupUpdate;
edouard@1586
   144
            on CannotDecrypt {
edouard@1523
   145
                do sendUpdateRequest;
edouard@1586
   146
                do sendBeacon;
edouard@1586
   147
            }
edouard@1523
   148
            on UpdateRequest
edouard@1523
   149
                do sendGroupUpdate;
edouard@1523
   150
            on Beacon(Identity partner){
edouard@1523
   151
                do sendHandshakeRequest(partner);
edouard@1523
   152
                go GroupedBeaconed(partner);
edouard@1523
   153
            }
edouard@1523
   154
            on HandshakeRequest(Identity partner) {
edouard@1523
   155
                if sameIdentities(partner, expected) {
edouard@1523
   156
                    // do nothing, to avoid sending handshake request twice 
edouard@1523
   157
                } else {
edouard@1523
   158
                    do sendHandshakeRequest(partner);
edouard@1523
   159
                }
edouard@1523
   160
                go HandshakingGrouped(partner);
edouard@1523
   161
            }
edouard@1588
   162
            on GroupUpdate(Identity partner, identity_list keys)
edouard@1588
   163
                do storeGroupUpdate(partner, keys);
edouard@1523
   164
            on Timeout go Grouped;
edouard@1523
   165
        }
edouard@1523
   166
edouard@1460
   167
        state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1586
   168
            // HandshakeRequest from same group are filtered in receive_sync_msg
edouard@1586
   169
            on Init{
edouard@1586
   170
                if keyElectionWon(partner) {
edouard@1586
   171
                    do notifyInitAddOtherDevice(partner);
edouard@1586
   172
                } else {
edouard@1586
   173
                    do notifyInitMoveOurDevice(partner);
edouard@1586
   174
                }
edouard@1586
   175
            }
edouard@1216
   176
            on HandshakeRejected(Identity partner) {
edouard@1216
   177
                do rejectHandshake(partner);             // stores rejection of partner
edouard@1216
   178
                go Grouped;
vb@563
   179
            }
edouard@1216
   180
            on HandshakeAccepted(Identity partner) {
edouard@1161
   181
                do acceptHandshake(partner); 
edouard@1586
   182
                if keyElectionWon(partner) {
edouard@1586
   183
                    do sendGroupKeys(partner);
edouard@1586
   184
                    do notifyAcceptedDeviceAdded(partner);
edouard@1586
   185
                    go Grouped;
edouard@1586
   186
                }
edouard@1586
   187
                go WaitForGroupKeysGrouped(partner);
edouard@1586
   188
            }
edouard@1586
   189
            on Cancel go Grouped;
edouard@1586
   190
            on Timeout {
edouard@1586
   191
                do notifyTimeout(expected);
edouard@1445
   192
                go Grouped;
edouard@1445
   193
            }
edouard@1586
   194
        }
edouard@1586
   195
edouard@1586
   196
        state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
edouard@1588
   197
            on GroupKeys(Identity partner, identity_list keys) {
edouard@1586
   198
                if sameIdentities(partner, expected) {
edouard@1586
   199
                    do storeGroupKeys(partner, keys);
edouard@1586
   200
                    do sendGroupUpdate;
edouard@1586
   201
                    do notifyAcceptedDeviceMoved(partner);
edouard@1586
   202
                    go Grouped;
edouard@1586
   203
                }
edouard@1586
   204
            }
edouard@1445
   205
            on Timeout {
edouard@1477
   206
                do notifyTimeout(expected);
edouard@1216
   207
                go Grouped;
edouard@1161
   208
            }
vb@563
   209
        }
Edouard@613
   210
vb@951
   211
        tag Init 1;
vb@951
   212
        tag Beacon 2;
vb@951
   213
        tag HandshakeRequest 3;
vb@951
   214
        tag GroupKeys 4;
Edouard@613
   215
    }
vb@563
   216
}
vb@563
   217