sync/sync.fsm
author Dirk Zimmermann <dz@pep.security>
Tue, 09 Apr 2019 16:02:46 +0200
branchIOS-1482
changeset 3480 689c15d6bef7
parent 3470 3f5f6d631953
child 3509 a9c0c6f31c56
permissions -rw-r--r--
IOS-1482 Xcode: Change organization name.
vb@2831
     1
// This file is under BSD License 2.0
vb@2831
     2
vb@2831
     3
// Sync protocol for p≡p
vb@3389
     4
// Copyright (c) 2016 - 2019, p≡p foundation
vb@2831
     5
vb@2831
     6
// Written by Volker Birk
vb@2831
     7
vb@2831
     8
include ./fsm.yml2
vb@2831
     9
vb@2831
    10
protocol Sync 1 {
vb@2831
    11
    // all messages have a timestamp, time out and are removed after timeout
vb@2831
    12
vb@2831
    13
    fsm KeySync 1 {
vb@2831
    14
        version 1, 2;
vb@2913
    15
vb@2831
    16
        state InitState {
vb@2831
    17
            on Init {
vb@2831
    18
                if deviceGrouped
vb@2831
    19
                    go Grouped;
vb@2831
    20
                go Sole;
vb@2831
    21
            }
vb@2831
    22
        }
vb@2831
    23
vb@2908
    24
        state Sole timeout=off {
vb@2831
    25
            on Init {
vb@2831
    26
                do openChallenge; // own challenge
vb@2865
    27
                send Beacon;
vb@2831
    28
            }
vb@2831
    29
vb@2831
    30
            on KeyGen
vb@2865
    31
                send Beacon;
vb@2831
    32
vb@2831
    33
            on CannotDecrypt // cry baby
vb@2865
    34
                send Beacon;
vb@2831
    35
vb@2831
    36
            on Beacon {
vb@2907
    37
                if weAreFirst {
vb@2907
    38
                    send Beacon;
vb@2907
    39
                }
vb@2907
    40
                else {
vb@2902
    41
                    do storeChallenge; // partner's challenge
vb@2902
    42
                    do openTransaction;
vb@2902
    43
                    do storeTransaction;
vb@2902
    44
                    send HandshakeRequest;
vb@2902
    45
                }
vb@2831
    46
            }
vb@2831
    47
vb@2831
    48
            on HandshakeRequest {
vb@2831
    49
                if challengeAccepted {
vb@2831
    50
                    do storeTransaction;
vb@2865
    51
                    send HandshakeAnswer;
vb@2831
    52
                    if partnerIsGrouped
vb@2831
    53
                        go HandshakingWithGroup;
vb@3345
    54
                    go HandshakingNew;
vb@2831
    55
                }
vb@2831
    56
            }
vb@3341
    57
vb@2831
    58
            on HandshakeAnswer
vb@3345
    59
                go HandshakingNew;
vb@2831
    60
        }
vb@2831
    61
vb@2831
    62
        // handshaking without existing Device group
vb@2831
    63
        state HandshakingNew {
vb@3470
    64
            on Init
vb@2831
    65
                do showSoleHandshake;
vb@2831
    66
vb@2831
    67
            // Cancel is Rollback
vb@2831
    68
            on Cancel {
vb@2865
    69
                send Rollback;
vb@2831
    70
                go Sole;
vb@2831
    71
            }
vb@2831
    72
vb@2831
    73
            on Rollback
vb@2831
    74
                go Sole;
vb@2831
    75
vb@2831
    76
            // Reject is CommitReject
vb@2831
    77
            on Reject {
vb@2865
    78
                send CommitReject;
vb@2831
    79
                do disable;
vb@2831
    80
                go End;
vb@2831
    81
            }
vb@2831
    82
vb@2831
    83
            on CommitReject {
vb@2831
    84
                do disable;
vb@2831
    85
                go End;
vb@2831
    86
            }
vb@2831
    87
vb@2831
    88
            // Accept is Phase1Commit
vb@2831
    89
            on Accept {
vb@3470
    90
                send CommitAcceptForGroup;
vb@2831
    91
                go HandshakingNewPhase1;
vb@2831
    92
            }
vb@2831
    93
vb@3470
    94
            on CommitAccept
vb@3470
    95
                go HandshakingNewPhase1Own;
vb@2831
    96
        }
vb@2831
    97
vb@2831
    98
        state HandshakingNewPhase1 {
vb@2831
    99
            on Rollback
vb@2831
   100
                go Sole;
vb@2831
   101
            
vb@2831
   102
            on CommitReject {
vb@2831
   103
                do disable;
vb@2831
   104
                go End;
vb@2831
   105
            }
vb@2831
   106
vb@3470
   107
            on CommitAcceptForGroup
vb@3470
   108
                go NewGroup;
vb@2831
   109
        }
vb@2831
   110
vb@2831
   111
        state HandshakingNewPhase1Own {
vb@2831
   112
            on Cancel {
vb@2865
   113
                send Rollback;
vb@2831
   114
                go Sole;
vb@2831
   115
            }
vb@2831
   116
vb@2831
   117
            on Reject {
vb@2865
   118
                send CommitReject;
vb@2831
   119
                do disable;
vb@2831
   120
                go End;
vb@2831
   121
            }
vb@2831
   122
vb@2831
   123
            on Accept
vb@3470
   124
                go NewGroup;
vb@2831
   125
        }
vb@2831
   126
vb@2831
   127
        state NewGroup {
vb@3390
   128
            on Init {
vb@3390
   129
                do prepareOwnKeys;
vb@2865
   130
                send GroupKeysAndClose; // we're not grouped yet, this is our own keys
vb@3390
   131
            }
vb@2831
   132
vb@2831
   133
            on GroupKeysAndClose {
vb@3406
   134
                if keyElectionWon
vb@2831
   135
                    do ownKeysAreGroupKeys;
vb@3406
   136
                else
vb@3406
   137
                    do receivedKeysAreGroupKeys;
vb@2831
   138
                go Grouped;
vb@2831
   139
            }
vb@2831
   140
        }
vb@2831
   141
vb@2831
   142
        state HandshakingWithGroup {
vb@2831
   143
            on Init
vb@2831
   144
                do showJoinGroupHandshake;
vb@2831
   145
vb@2831
   146
            // Cancel is Rollback
vb@2831
   147
            on Cancel {
vb@2865
   148
                send Rollback;
vb@2831
   149
                go Sole;
vb@2831
   150
            }
vb@2831
   151
vb@2831
   152
            on Rollback
vb@2831
   153
                go Sole;
vb@2831
   154
vb@2831
   155
            // Reject is CommitReject
vb@2831
   156
            on Reject {
vb@2865
   157
                send CommitReject;
vb@2831
   158
                do disable;
vb@2831
   159
                go End;
vb@2831
   160
            }
vb@2831
   161
vb@2831
   162
            on CommitReject {
vb@2831
   163
                do disable;
vb@2831
   164
                go End;
vb@2831
   165
            }
vb@2831
   166
vb@2831
   167
            // Accept is Phase1Commit
vb@2831
   168
            on Accept {
vb@2865
   169
                send CommitAccept;
vb@2831
   170
                go HandshakingJoinPhase1;
vb@2831
   171
            }
vb@2831
   172
vb@3439
   173
            on CommitAcceptForGroup
vb@2831
   174
                go HandshakingJoinPhase1Own;
vb@2831
   175
        }
vb@2831
   176
vb@2831
   177
        state HandshakingJoinPhase1 {
vb@2831
   178
            on Rollback
vb@2831
   179
                go Sole;
vb@2831
   180
            
vb@2831
   181
            on CommitReject {
vb@2831
   182
                do disable;
vb@2831
   183
                go End;
vb@2831
   184
            }
vb@2831
   185
vb@3439
   186
            on CommitAcceptForGroup
vb@2831
   187
                go JoinGroup;
vb@2831
   188
        }
vb@2831
   189
vb@2831
   190
        state HandshakingJoinPhase1Own {
vb@2831
   191
            on Cancel {
vb@2865
   192
                send Rollback;
vb@2831
   193
                go Sole;
vb@2831
   194
            }
vb@2831
   195
vb@2831
   196
            on Reject {
vb@2865
   197
                send CommitReject;
vb@2831
   198
                do disable;
vb@2831
   199
                go End;
vb@2831
   200
            }
vb@2831
   201
vb@2831
   202
            on Accept
vb@2831
   203
                go JoinGroup;
vb@2831
   204
        }
vb@2831
   205
vb@2831
   206
        state JoinGroup {
vb@2831
   207
            on GroupKeysAndClose {
vb@2865
   208
                send GroupKeys; // first send own keys
vb@2831
   209
                do saveGroupKeys; // then store new group keys
vb@2831
   210
                go Grouped;
vb@2831
   211
            }
vb@2831
   212
        }
vb@2831
   213
vb@2908
   214
        state Grouped timeout=off {
vb@2831
   215
            on GroupKeys
vb@2831
   216
                do saveGroupKeys;
vb@2831
   217
vb@2831
   218
            on KeyGen
vb@2865
   219
                send GroupKeys;
vb@2831
   220
vb@2831
   221
            on Beacon
vb@2865
   222
                send HandshakeRequest;
vb@2831
   223
vb@2831
   224
            on HandshakeAnswer
vb@2831
   225
                go HandshakingGrouped;
vb@2831
   226
        }
vb@2831
   227
vb@2831
   228
        state HandshakingGrouped {
vb@2831
   229
            on Init
vb@2831
   230
                do showGroupedHandshake;
vb@2831
   231
    
vb@2831
   232
            // Cancel is Rollback
vb@2831
   233
            on Cancel {
vb@2865
   234
                send Rollback;
vb@2831
   235
                go Grouped;
vb@2831
   236
            }
vb@2831
   237
vb@2831
   238
            on Rollback
vb@2831
   239
                go Grouped;
vb@2831
   240
vb@2831
   241
            // Reject is CommitReject
vb@2831
   242
            on Reject {
vb@2865
   243
                send CommitReject;
vb@2831
   244
                go Grouped;
vb@2831
   245
            }
vb@2831
   246
vb@2831
   247
            on CommitReject
vb@2831
   248
                go Grouped;
vb@2831
   249
vb@2831
   250
            // Accept is Phase1Commit
vb@2831
   251
            on Accept {
vb@3439
   252
                send CommitAcceptForGroup;
vb@2831
   253
                go HandshakingGroupedPhase1;
vb@2831
   254
            }
vb@2831
   255
vb@2831
   256
            on CommitAccept
vb@2831
   257
                go HandshakingGroupedPhase1Own;
vb@2831
   258
vb@2831
   259
            on GroupKeys
vb@2831
   260
                do saveGroupKeys;
vb@2831
   261
        }
vb@2831
   262
vb@2831
   263
        state HandshakingGroupedPhase1 {
vb@2831
   264
            on Rollback
vb@2831
   265
                go Grouped;
vb@2831
   266
vb@2831
   267
            on CommitReject
vb@2831
   268
                go Grouped;
vb@2831
   269
vb@2831
   270
            on CommitAccept {
vb@2865
   271
                send GroupKeysAndClose;
vb@2831
   272
                go Grouped;
vb@2831
   273
            }
vb@2831
   274
vb@2831
   275
            on GroupKeys
vb@2831
   276
                do saveGroupKeys;
vb@2831
   277
        }
vb@2831
   278
vb@2831
   279
        state HandshakingGroupedPhase1Own {
vb@2831
   280
            on Cancel {
vb@2865
   281
                send Rollback;
vb@2831
   282
                go Grouped;
vb@2831
   283
            }
vb@2831
   284
vb@2831
   285
            on Reject {
vb@2865
   286
                send CommitReject;
vb@2831
   287
                go Grouped;
vb@2831
   288
            }
vb@2831
   289
vb@2831
   290
            on Accept {
vb@2865
   291
                send GroupKeysAndClose;
vb@2831
   292
                go Grouped;
vb@2831
   293
            }
vb@2831
   294
vb@2831
   295
            on GroupKeys
vb@2831
   296
                do saveGroupKeys;
vb@2831
   297
        }
vb@2831
   298
 
vb@3384
   299
        external Accept 129;
vb@3384
   300
        external Reject 130;
vb@3384
   301
        external Cancel 131;
vb@2831
   302
vb@2867
   303
        // beacons are always broadcasted
vb@2867
   304
vb@2876
   305
        message Beacon 2, type=broadcast, security=unencrypted {
vb@2831
   306
            field TID challenge;
vb@2831
   307
            auto Version version;
vb@2831
   308
        }
vb@2831
   309
vb@2876
   310
        message HandshakeRequest 3, security=untrusted {
vb@2831
   311
            field TID challenge;
vb@2831
   312
            auto Version version;
vb@2831
   313
            field TID transaction;
vb@2831
   314
            field bool is_group;
vb@2831
   315
        }
vb@2831
   316
vb@3381
   317
        message HandshakeAnswer 4, security=untrusted {
vb@3379
   318
            auto Version version;
vb@2831
   319
            field TID transaction;
vb@2831
   320
        }
vb@2831
   321
vb@2876
   322
        message Rollback 5, security=untrusted {
vb@2831
   323
            field TID transaction;
vb@2831
   324
        }
vb@2831
   325
vb@2876
   326
        message CommitReject 6, security=untrusted {
vb@2831
   327
            field TID transaction;
vb@2831
   328
        }
vb@2831
   329
vb@2831
   330
        message CommitAccept 7 {
vb@2831
   331
            field TID transaction;
vb@2831
   332
        }
vb@2831
   333
vb@3439
   334
        message CommitAcceptForGroup 8 {
vb@3439
   335
            field TID transaction;
vb@3439
   336
        }
vb@3439
   337
vb@3439
   338
        message GroupKeysAndClose 9, security=attach_own_keys {
vb@2831
   339
            field TID transaction;
vb@3390
   340
            field IdentityList ownIdentities;
vb@2831
   341
        }
vb@2831
   342
vb@3439
   343
        message GroupKeys 10, security=attach_own_keys {
vb@3390
   344
            field IdentityList ownIdentities;
vb@2831
   345
        }
vb@2831
   346
    }
vb@2831
   347
}
vb@2831
   348