sync/devicegroup.fsm
author Edouard Tisserant <edouard@pep-project.org>
Fri, 09 Dec 2016 01:36:57 +0100
changeset 1477 c0d761ae1fd9
parent 1460 66ceb5a7f718
child 1513 e7f7e42385b5
permissions -rw-r--r--
sync: obey new app notification enum names, this time with corresponding actions generated
vb@563
     1
// DeviceGroup protocol for p≡p
vb@563
     2
vb@563
     3
// Copyleft (c) 2016, p≡p foundation
vb@563
     4
vb@563
     5
// Written by Volker Birk
vb@563
     6
vb@563
     7
include ./fsm.yml2
vb@563
     8
vb@563
     9
protocol DeviceGroup {
vb@563
    10
    // all messages have a timestamp, time out and are removed after timeout
vb@563
    11
vb@1047
    12
    broadcast sendBeacon;
edouard@1281
    13
    broadcast sendGroupUpdate;
edouard@1297
    14
    broadcast sendUpdateRequest;
vb@1097
    15
    unencrypted sendBeacon;
vb@1047
    16
vb@807
    17
    fsm DeviceState filename=sync {
vb@951
    18
        condition storedGroupKeys();
vb@951
    19
        condition keyElectionWon(Identity partner);
vb@951
    20
vb@624
    21
        state InitState {
vb@624
    22
            on Init {
vb@951
    23
                if storedGroupKeys()
vb@624
    24
                    go Grouped;
vb@624
    25
                go Sole;
vb@624
    26
            }
vb@563
    27
        }
vb@563
    28
vb@1409
    29
        state Sole end=1 {
vb@944
    30
            on KeyGen // injected by generate_keypair()
vb@1097
    31
                do sendBeacon;
vb@563
    32
            on CannotDecrypt
vb@566
    33
                do sendBeacon;  // cry, baby
Edouard@594
    34
            on Beacon(Identity partner) // this event will not happen for already
vb@571
    35
                                        // rejected partners
vb@582
    36
                do sendHandshakeRequest(partner);
Edouard@594
    37
            on HandshakeRequest(Identity partner) {
vb@582
    38
                do sendHandshakeRequest(partner);
vb@563
    39
                go HandshakingSole(partner);
vb@563
    40
            }
vb@563
    41
        }
vb@563
    42
edouard@1460
    43
        state HandshakingSole timeout=600 (Identity expected) {
edouard@1477
    44
            on Init{
edouard@1477
    45
                if keyElectionWon(partner) {    // an already existing group
edouard@1477
    46
                    do notifyInitFormGroup(partner);
edouard@1477
    47
                } else {
edouard@1477
    48
                    do notifyInitAddOurDevice(partner);
edouard@1477
    49
                }
edouard@1477
    50
            }
edouard@1477
    51
Edouard@594
    52
            on HandshakeRejected(Identity partner) {
edouard@1161
    53
                do rejectHandshake(partner);             // stores rejection of partner
vb@563
    54
                go Sole;
vb@563
    55
            }
Edouard@594
    56
            on HandshakeAccepted(Identity partner) {
edouard@1161
    57
                do acceptHandshake(partner); 
vb@567
    58
                if keyElectionWon(partner) {    // an already existing group
vb@567
    59
                                                // always wins
edouard@1161
    60
                    do sendGroupKeys(partner);
edouard@1477
    61
                    do notifyAcceptedGroupCreated(partner);
vb@563
    62
                    go Grouped;
vb@563
    63
                }
edouard@1460
    64
                go WaitForGroupKeysSole(partner);
vb@563
    65
            }
edouard@1445
    66
            on Cancel go Sole;
edouard@1445
    67
            on Timeout {
edouard@1477
    68
                do notifyTimeout(expected);
edouard@1445
    69
                go Sole;
edouard@1445
    70
            }
vb@563
    71
        }
vb@563
    72
    
edouard@1460
    73
        state WaitForGroupKeysSole timeout=600 (Identity expected) {
vb@711
    74
            on GroupKeys(Identity partner, Stringlist keys) {
edouard@1460
    75
                // TODO ensure partner == expected
Edouard@605
    76
                do storeGroupKeys(partner, keys);
edouard@1477
    77
                do notifyAcceptedDeviceAdded(partner);
vb@563
    78
                go Grouped;
vb@563
    79
            }
edouard@1445
    80
            on Timeout {
edouard@1477
    81
                do notifyTimeout(expected);
vb@569
    82
                go Sole;
vb@569
    83
            }
vb@563
    84
        }
vb@563
    85
vb@1409
    86
        state Grouped end=1 {
edouard@1297
    87
            on Init 
edouard@1297
    88
                do enterGroup;
vb@563
    89
            on KeyGen
edouard@1281
    90
                do sendGroupUpdate;
edouard@1297
    91
            on CannotDecrypt
edouard@1297
    92
                do sendUpdateRequest; // TODO: narrow request to missing key
edouard@1297
    93
            on UpdateRequest
edouard@1297
    94
                do sendGroupUpdate;
edouard@1216
    95
            on Beacon(Identity partner)
edouard@1216
    96
                do sendHandshakeRequest(partner);
Edouard@594
    97
            on HandshakeRequest(Identity partner) {
vb@582
    98
                do sendHandshakeRequest(partner);
edouard@1216
    99
                go HandshakingGrouped(partner);
edouard@1216
   100
            }
edouard@1281
   101
            on GroupUpdate(Identity partner, Stringlist keys)
edouard@1236
   102
                do storeGroupKeys(partner, keys);
edouard@1216
   103
        }
edouard@1216
   104
edouard@1460
   105
        state HandshakingGrouped timeout=600 (Identity expected) {
edouard@1216
   106
            on Init
edouard@1477
   107
                do notifyInitAddOurDevice(partner);
edouard@1216
   108
            on HandshakeRejected(Identity partner) {
edouard@1216
   109
                do rejectHandshake(partner);             // stores rejection of partner
edouard@1216
   110
                go Grouped;
vb@563
   111
            }
edouard@1216
   112
            on HandshakeAccepted(Identity partner) {
edouard@1161
   113
                do acceptHandshake(partner); 
edouard@1216
   114
edouard@1216
   115
                // an already existing group always wins
vb@711
   116
                do sendGroupKeys(partner);
edouard@1445
   117
edouard@1445
   118
                go Grouped;
edouard@1445
   119
            }
edouard@1445
   120
            on Timeout {
edouard@1477
   121
                do notifyTimeout(expected);
edouard@1216
   122
                go Grouped;
edouard@1161
   123
            }
vb@563
   124
        }
Edouard@613
   125
vb@951
   126
        tag Init 1;
vb@951
   127
        tag Beacon 2;
vb@951
   128
        tag HandshakeRequest 3;
vb@951
   129
        tag GroupKeys 4;
Edouard@613
   130
    }
vb@563
   131
}
vb@563
   132