sync/sync.fsm
author Volker Birk <vb@pep-project.org>
Thu, 16 Jan 2020 15:04:04 +0100
branchsync
changeset 4337 7e8015c705ae
parent 4289 79af186cae4e
child 4338 7a9de0786596
permissions -rw-r--r--
explicit debug messages in fsm
     1 // This file is under BSD License 2.0
     2 
     3 // Sync protocol for p≡p
     4 // Copyright (c) 2016-2019, p≡p foundation
     5 
     6 // Written by Volker Birk
     7 
     8 include ./fsm.yml2
     9 
    10 protocol Sync 1 {
    11     // all messages have a timestamp, time out and are removed after timeout
    12 
    13     fsm KeySync 1, threshold=300 {
    14         version 1, 2;
    15 
    16         state InitState {
    17             on Init {
    18                 if deviceGrouped
    19                     go Grouped;
    20                 do newChallengeAndNegotiationBase;
    21                 send Beacon;
    22                 go Sole;
    23             }
    24         }
    25 
    26         state Sole timeout=off {
    27             on Init {
    28                 do showBeingSole;
    29             }
    30 
    31             on KeyGen {
    32                 send Beacon;
    33             }
    34 
    35             on CannotDecrypt { // cry baby
    36                 send Beacon;
    37             }
    38 
    39             on Beacon {
    40                 if sameChallenge {
    41                     debug > this is our own Beacon; ignore
    42                 }
    43                 else {
    44                     if weAreOfferer {
    45                         do useOwnChallenge;
    46                         send Beacon;
    47                     }
    48                     else /* we are requester */ {
    49                         do openNegotiation;
    50                         do tellWeAreNotGrouped;
    51                         // requester is sending NegotiationRequest
    52                         send NegotiationRequest;
    53                         do useOwnChallenge;
    54                     }
    55                 }
    56             }
    57 
    58             // we get this from another sole device
    59             on NegotiationRequest {
    60                 if sameChallenge { // challenge accepted
    61                     if sameNegotiation {
    62                         // this is our own NegotiationRequest; ignore
    63                     }
    64                     else {
    65                         do storeNegotiation;
    66                         // offerer is accepting by confirming NegotiationOpen
    67                         send NegotiationOpen;
    68                         go HandshakingOfferer;
    69                     }
    70                 }
    71             }
    72 
    73             // we get this from an existing device group
    74             on NegotiationRequestGrouped {
    75                 if sameChallenge { // challenge accepted
    76                     do storeNegotiation;
    77                     // offerer is accepting by confirming NegotiationOpen
    78                     send NegotiationOpen;
    79                     go HandshakingToJoin;
    80                 }
    81             }
    82 
    83             on NegotiationOpen if sameNegotiationAndPartner {
    84                 // requester is receiving NegotiationOpen
    85                 do storeNegotiation;
    86                 go HandshakingRequester;
    87             }
    88         }
    89 
    90         // handshaking without existing Device group
    91         state HandshakingOfferer timeout=600 {
    92             on Init
    93                 do showSoleHandshake;
    94 
    95             // Cancel is Rollback
    96             on Cancel {
    97                 send Rollback;
    98                 go Sole;
    99             }
   100 
   101             on Rollback if sameNegotiationAndPartner
   102                 go Sole;
   103 
   104             // Reject is CommitReject
   105             on Reject {
   106                 send CommitReject;
   107                 do disable;
   108                 go End;
   109             }
   110 
   111             on CommitReject if sameNegotiationAndPartner {
   112                 do disable;
   113                 go End;
   114             }
   115 
   116             // Accept means init Phase1Commit
   117             on Accept {
   118                 do trustThisKey;
   119                 send CommitAcceptOfferer;
   120                 go HandshakingPhase1Offerer;
   121             }
   122 
   123             // got a CommitAccept from requester
   124             on CommitAcceptRequester if sameNegotiationAndPartner
   125                 go HandshakingPhase2Offerer;
   126         }
   127 
   128         // handshaking without existing Device group
   129         state HandshakingRequester timeout=600 {
   130             on Init
   131                 do showSoleHandshake;
   132 
   133             // Cancel is Rollback
   134             on Cancel {
   135                 send Rollback;
   136                 go Sole;
   137             }
   138 
   139             on Rollback if sameNegotiationAndPartner
   140                 go Sole;
   141 
   142             // Reject is CommitReject
   143             on Reject {
   144                 send CommitReject;
   145                 do disable;
   146                 go End;
   147             }
   148 
   149             on CommitReject if sameNegotiationAndPartner {
   150                 do disable;
   151                 go End;
   152             }
   153 
   154             // Accept means init Phase1Commit
   155             on Accept {
   156                 do trustThisKey;
   157                 send CommitAcceptRequester;
   158                 go HandshakingPhase1Requester;
   159             }
   160 
   161             // got a CommitAccept from offerer
   162             on CommitAcceptOfferer if sameNegotiationAndPartner
   163                 go HandshakingPhase2Requester;
   164         }
   165 
   166         state HandshakingPhase1Offerer {
   167             on Rollback if sameNegotiationAndPartner {
   168                 do untrustThisKey;
   169                 go Sole;
   170             }
   171             
   172             on CommitReject if sameNegotiationAndPartner {
   173                 do untrustThisKey;
   174                 do disable;
   175                 go End;
   176             }
   177 
   178             on CommitAcceptRequester if sameNegotiationAndPartner {
   179                 go FormingGroupOfferer;
   180             }
   181         }
   182 
   183         state HandshakingPhase1Requester {
   184             on Rollback if sameNegotiationAndPartner {
   185                 do untrustThisKey;
   186                 go Sole;
   187             }
   188             
   189             on CommitReject if sameNegotiationAndPartner {
   190                 do untrustThisKey;
   191                 do disable;
   192                 go End;
   193             }
   194 
   195             on CommitAcceptOfferer if sameNegotiationAndPartner {
   196                 go FormingGroupRequester;
   197             }
   198         }
   199 
   200         state HandshakingPhase2Offerer {
   201             on Cancel {
   202                 send Rollback;
   203                 go Sole;
   204             }
   205 
   206             on Reject {
   207                 send CommitReject;
   208                 do disable;
   209                 go End;
   210             }
   211 
   212             on Accept {
   213                 do trustThisKey;
   214                 send CommitAcceptOfferer;
   215                 go FormingGroupOfferer;
   216             }
   217         }
   218 
   219         state HandshakingPhase2Requester {
   220             on Cancel {
   221                 send Rollback;
   222                 go Sole;
   223             }
   224 
   225             on Reject {
   226                 send CommitReject;
   227                 do disable;
   228                 go End;
   229             }
   230 
   231             on Accept {
   232                 do trustThisKey;
   233                 send CommitAcceptRequester;
   234                 go FormingGroupRequester;
   235             }
   236         }
   237 
   238         state FormingGroupOfferer {
   239             on Init {
   240                 do prepareOwnKeys;
   241                 send OwnKeysOfferer; // we're not grouped yet, this is our own keys
   242             }
   243 
   244             on Cancel {
   245                 send Rollback;
   246                 go Sole;
   247             }
   248 
   249             on Rollback
   250                 go Sole;
   251 
   252             on OwnKeysRequester if sameNegotiationAndPartner {
   253                 do saveGroupKeys;
   254                 do receivedKeysAreDefaultKeys;
   255                 do showGroupCreated;
   256                 go Grouped;
   257             }
   258         }
   259 
   260         state FormingGroupRequester {
   261             on Cancel {
   262                 send Rollback;
   263                 go Sole;
   264             }
   265 
   266             on Rollback
   267                 go Sole;
   268 
   269             on OwnKeysOfferer if sameNegotiationAndPartner {
   270                 do saveGroupKeys;
   271                 do prepareOwnKeys;
   272                 do ownKeysAreDefaultKeys;
   273                 send OwnKeysRequester;
   274                 do showGroupCreated;
   275                 go Grouped;
   276             }
   277         }
   278 
   279         state Grouped timeout=off {
   280             on Init {
   281                 do newChallengeAndNegotiationBase;
   282                 do showBeingInGroup;
   283             }
   284 
   285             on GroupKeysUpdate if fromGroupMember // double check
   286                 do saveGroupKeys;
   287 
   288             on KeyGen {
   289                 do prepareOwnKeys;
   290                 send GroupKeysUpdate;
   291             }
   292 
   293             on Beacon {
   294                 do openNegotiation;
   295                 do tellWeAreGrouped;
   296                 send NegotiationRequestGrouped;
   297                 do useOwnChallenge;
   298             }
   299 
   300             on NegotiationOpen if sameNegotiationAndPartner {
   301                 do storeNegotiation;
   302                 do useThisKey;
   303                 send GroupHandshake;
   304                 go HandshakingGrouped;
   305             }
   306 
   307             on GroupHandshake {
   308                 do storeNegotiation;
   309                 do storeThisKey;
   310                 go HandshakingGrouped;
   311             }
   312 
   313             on GroupTrustThisKey if fromGroupMember // double check
   314                 do trustThisKey;
   315 
   316             on GroupKeyResetRequired {
   317                 do ledGroupKeyReset;
   318                 send GroupKeyReset;
   319             }
   320 
   321             // this is for a leaving group member
   322             on GroupKeyResetRequiredAndDisable {
   323                 send InitUnledGroupKeyReset;
   324                 go DisableOnInitUnledGroupKeyReset;
   325             }
   326 
   327             on InitUnledGroupKeyReset {
   328                 // unled group key reset; new group keys will be elected
   329                 do unledGroupKeyReset;
   330                 send GroupKeyReset;
   331             }
   332 
   333             on GroupKeyReset if fromGroupMember { // double check
   334                 do saveGroupKeys;
   335                 if isLedGroupKeyReset {
   336                     // led group key reset is executed without questions
   337                     do receivedKeysAreDefaultKeys;
   338                 }
   339                 else {
   340                     // unled group key reset; election takes place
   341                     if keyElectionWon {
   342                         // this is already the case:
   343                         // do ownKeysAreDefaultKeys;
   344                     }
   345                     else {
   346                         do receivedKeysAreDefaultKeys;
   347                     }
   348                 }
   349             }
   350         }
   351 
   352         state DisableOnInitUnledGroupKeyReset {
   353             on InitUnledGroupKeyReset
   354                 do disable;
   355         }
   356 
   357         // sole device handshaking with group
   358         state HandshakingToJoin {
   359             on Init
   360                 do showJoinGroupHandshake;
   361 
   362             // Cancel is Rollback
   363             on Cancel {
   364                 send Rollback;
   365                 go Sole;
   366             }
   367 
   368             on Rollback if sameNegotiationAndPartner
   369                 go Sole;
   370 
   371             // Reject is CommitReject
   372             on Reject {
   373                 send CommitReject;
   374                 do disable;
   375                 go End;
   376             }
   377 
   378             on CommitAcceptForGroup if sameNegotiationAndPartner
   379                 go HandshakingToJoinPhase2;
   380 
   381             on CommitReject if sameNegotiationAndPartner {
   382                 do disable;
   383                 go End;
   384             }
   385 
   386             // Accept is Phase1Commit
   387             on Accept {
   388                 do trustThisKey;
   389                 send CommitAccept;
   390                 go HandshakingToJoinPhase1;
   391             }
   392         }
   393 
   394         state HandshakingToJoinPhase1 {
   395             on Rollback if sameNegotiationAndPartner
   396                 go Sole;
   397             
   398             on CommitReject if sameNegotiationAndPartner {
   399                 do disable;
   400                 go End;
   401             }
   402 
   403             on CommitAcceptForGroup if sameNegotiationAndPartner
   404                 go JoiningGroup;
   405         }
   406 
   407         state HandshakingToJoinPhase2 {
   408             on Cancel {
   409                 send Rollback;
   410                 go Sole;
   411             }
   412 
   413             on Reject {
   414                 send CommitReject;
   415                 do disable;
   416                 go End;
   417             }
   418 
   419             on Accept {
   420                 do trustThisKey;
   421                 send CommitAccept;
   422                 go JoiningGroup;
   423             }
   424         }
   425 
   426         state JoiningGroup {
   427             on GroupKeysForNewMember if sameNegotiationAndPartner {
   428                 do saveGroupKeys;
   429                 do receivedKeysAreDefaultKeys;
   430                 do prepareOwnKeys;
   431                 send GroupKeysAndClose;
   432                 do showDeviceAdded;
   433                 go Grouped;
   434             }
   435         }
   436 
   437         state HandshakingGrouped {
   438             on Init
   439                 do showGroupedHandshake;
   440     
   441             // Cancel is Rollback
   442             on Cancel {
   443                 send Rollback;
   444                 go Grouped;
   445             }
   446 
   447             on Rollback if sameNegotiationAndPartner
   448                 go Grouped;
   449 
   450             // Reject is CommitReject
   451             on Reject {
   452                 send CommitReject;
   453                 go Grouped;
   454             }
   455 
   456             on CommitReject if sameNegotiationAndPartner
   457                 go Grouped;
   458 
   459             // Accept is Phase1Commit
   460             on Accept {
   461                 do trustThisKey;
   462                 go HandshakingGroupedPhase1;
   463             }
   464 
   465             on CommitAccept if sameNegotiationAndPartner
   466                 go HandshakingGroupedPhase2;
   467 
   468             on GroupTrustThisKey if fromGroupMember { // double check
   469                 do trustThisKey;
   470                 if sameNegotiation
   471                     go Grouped;
   472             }
   473 
   474             on GroupKeysUpdate if fromGroupMember // double check
   475                 do saveGroupKeys;
   476         }
   477 
   478         state HandshakingGroupedPhase1 {
   479             on Init {
   480                 send GroupTrustThisKey;
   481                 send CommitAcceptForGroup;
   482             }
   483 
   484             on Rollback if sameNegotiationAndPartner
   485                 go Grouped;
   486 
   487             on CommitReject if sameNegotiationAndPartner
   488                 go Grouped;
   489 
   490             on CommitAccept if sameNegotiationAndPartner {
   491                 do prepareOwnKeys;
   492                 send GroupKeysForNewMember;
   493                 do showDeviceAccepted;
   494                 go Grouped;
   495             }
   496 
   497             on GroupTrustThisKey if fromGroupMember // double check
   498                 do trustThisKey;
   499 
   500             on GroupKeysUpdate if fromGroupMember // double check
   501                 do saveGroupKeys;
   502             
   503             on GroupKeysAndClose if fromGroupMember { // double check
   504                 do saveGroupKeys;
   505                 go Grouped;
   506             }
   507         }
   508 
   509         state HandshakingGroupedPhase2 {
   510             on Cancel {
   511                 send Rollback;
   512                 go Grouped;
   513             }
   514 
   515             on Reject {
   516                 send CommitReject;
   517                 go Grouped;
   518             }
   519 
   520             on Accept {
   521                 do trustThisKey;
   522                 send GroupTrustThisKey;
   523                 do prepareOwnKeys;
   524                 send GroupKeysForNewMember;
   525                 do showDeviceAccepted;
   526                 go Grouped;
   527             }
   528 
   529             on GroupTrustThisKey if fromGroupMember // double check
   530                 do trustThisKey;
   531 
   532             on GroupKeysUpdate if fromGroupMember // double check
   533                 do saveGroupKeys;
   534             
   535             on GroupKeysAndClose if fromGroupMember { // double check
   536                 do saveGroupKeys;
   537                 go Grouped;
   538             }
   539         }
   540  
   541         external Accept 129;
   542         external Reject 130;
   543         external Cancel 131;
   544 
   545         // beacons are always broadcasted
   546 
   547         message Beacon 2, type=broadcast, security=unencrypted {
   548             field TID challenge;
   549             auto Version version;
   550         }
   551 
   552         message NegotiationRequest 3, security=untrusted {
   553             field TID challenge;
   554             auto Version version;
   555             field TID negotiation;
   556             field bool is_group;
   557         }
   558 
   559         message NegotiationOpen 4, security=untrusted {
   560             auto Version version;
   561             field TID negotiation;
   562         }
   563 
   564         message Rollback 5, security=untrusted {
   565             field TID negotiation;
   566         }
   567 
   568         message CommitReject 6, security=untrusted {
   569             field TID negotiation;
   570         }
   571 
   572         message CommitAcceptOfferer 7, security=untrusted {
   573             field TID negotiation;
   574         }
   575 
   576         message CommitAcceptRequester 8, security=untrusted {
   577             field TID negotiation;
   578         }
   579 
   580         message CommitAccept 9, security=untrusted {
   581             field TID negotiation;
   582         }
   583 
   584         message CommitAcceptForGroup 10, security=untrusted {
   585             field TID negotiation;
   586         }
   587 
   588         // default: security=truste
   589         // messages are only accepted when coming from the device group
   590         message GroupTrustThisKey 11 {
   591             field Hash key;
   592             field TID negotiation;
   593         }
   594 
   595         // trust in future
   596         message GroupKeysForNewMember 12, security=attach_own_keys_for_new_member {
   597             field IdentityList ownIdentities;
   598         }
   599 
   600         message GroupKeysAndClose 13, security=attach_own_keys_for_new_member {
   601             field IdentityList ownIdentities;
   602         }
   603 
   604         message OwnKeysOfferer 14, security=attach_own_keys_for_new_member {
   605             field IdentityList ownIdentities;
   606         }
   607 
   608         message OwnKeysRequester 15, security=attach_own_keys_for_new_member {
   609             field IdentityList ownIdentities;
   610         }
   611 
   612         // grouped handshake
   613         message NegotiationRequestGrouped 16, security=untrusted {
   614             field TID challenge;
   615             auto Version version;
   616             field TID negotiation;
   617             field bool is_group;
   618         }
   619 
   620         message GroupHandshake 17 {
   621             field TID negotiation;
   622             field Hash key;
   623         }
   624 
   625         // update group
   626         message GroupKeysUpdate 18, security=attach_own_keys_for_group {
   627             field IdentityList ownIdentities;
   628         }
   629 
   630         // initiate unled group key reset
   631         message InitUnledGroupKeyReset 19 {
   632         }
   633 
   634         message GroupKeyReset 20, security=attach_own_keys_for_group {
   635             field TID challenge;
   636             // set this flag for led group key reset; delivered group keys will
   637             // be accepted by all group members; if not set group keys will be
   638             // elected
   639             field bool led;
   640             field IdentityList ownIdentities;
   641         }
   642     }
   643 }
   644