sync/devicegroup.fsm
author Thomas
Wed, 24 May 2017 15:19:41 +0200
branchtest_diphoton
changeset 1804 775bb90eccd5
parent 1749 32084f52dada
permissions -rw-r--r--
Add current user GPG4Win lookup
     1 // This file is under GNU General Public License 3.0
     2 // see LICENSE.txt
     3 
     4 // DeviceGroup protocol for p≡p
     5 
     6 // Copyleft (c) 2016, p≡p foundation
     7 
     8 // Written by Volker Birk
     9 
    10 include ./fsm.yml2
    11 
    12 protocol DeviceGroup {
    13     // all messages have a timestamp, time out and are removed after timeout
    14 
    15     broadcast sendBeacon;
    16     broadcast sendGroupUpdate;
    17     broadcast sendUpdateRequest;
    18     unencrypted sendBeacon;
    19 
    20     fsm DeviceState filename=sync {
    21         condition deviceGrouped();
    22         condition keyElectionWon(Identity partner);
    23         condition sameIdentities(Identity a, Identity b);
    24         condition sameKeyAndAddress(Identity a, Identity b);
    25 
    26         state InitState {
    27             on Init {
    28                 if deviceGrouped()
    29                     go Grouped;
    30                 go Sole;
    31             }
    32         }
    33 
    34         state Sole end=1 {
    35             on KeyGen {
    36                 do sendBeacon;
    37                 go SoleWaiting;
    38             }
    39             on CannotDecrypt {
    40                 do sendBeacon;
    41                 go SoleWaiting;
    42             }
    43             on Beacon(Identity partner){
    44                 do sendHandshakeRequest(partner);
    45                 go SoleBeaconed(partner);
    46             }
    47             on HandshakeRequest(Identity partner) {
    48                 do sendHandshakeRequest(partner);
    49                 go HandshakingSole(partner);
    50             }
    51         }
    52 
    53         // copy of sole state with a timeout to enable fast polling for a second
    54         // TODO use more YSLT power here (substates ?) 
    55         state SoleWaiting timeout=60 {
    56             on KeyGen {
    57                 do sendBeacon;
    58             }
    59             on CannotDecrypt {
    60                 do sendBeacon;
    61             }
    62             on Beacon(Identity partner){
    63                 do sendHandshakeRequest(partner);
    64                 go SoleBeaconed(partner);
    65             }
    66             on HandshakeRequest(Identity partner) {
    67                 do sendHandshakeRequest(partner);
    68                 go HandshakingSole(partner);
    69             }
    70             on Timeout go Sole;
    71         }
    72 
    73         state SoleBeaconed timeout=600 (Identity expected) {
    74             on KeyGen{
    75                 do sendBeacon;
    76                 go Sole;
    77             }
    78             on CannotDecrypt{
    79                 do sendBeacon;
    80                 go Sole;
    81             }
    82             on Beacon(Identity partner) {
    83                 do sendHandshakeRequest(partner);
    84                 go SoleBeaconed(partner);
    85             }
    86             on HandshakeRequest(Identity partner) {
    87                 if sameIdentities(partner, expected) {
    88                     // do nothing, to avoid sending handshake request twice 
    89                 } else {
    90                     do sendHandshakeRequest(partner);
    91                 }
    92                 go HandshakingSole(partner);
    93             }
    94             on Timeout go Sole;
    95         }
    96 
    97         state HandshakingSole timeout=600 (Identity expected) {
    98             on Init{
    99                 if keyElectionWon(expected) {
   100                     do notifyInitFormGroup(expected);
   101                 } else {
   102                     do notifyInitAddOurDevice(expected);
   103                 }
   104             }
   105             on HandshakeRejected(Identity partner) {
   106                 do rejectHandshake(partner);
   107                 go Sole;
   108             }
   109             on HandshakeAccepted(Identity partner) {
   110                 if sameIdentities(partner, expected) {
   111                     do acceptHandshake(partner); 
   112                     if keyElectionWon(partner) {
   113                         do makeGroup;
   114                         do sendGroupKeys(partner);
   115                         do renewUUID;
   116                         do notifyAcceptedGroupCreated(partner);
   117                         go Grouped;
   118                     }
   119                     go WaitForGroupKeysSole(partner);
   120                 }
   121                 go Sole;
   122             }
   123             on Cancel go Sole;
   124             on GroupKeys(Identity partner, GroupKeys groupkeys) {
   125                 if keyElectionWon(expected) {
   126                     // not supposed to receive groupkeys - ignore
   127                 } else {
   128                     // UUID changes in between, so we can only check for same address and fpr
   129                     if sameKeyAndAddress(partner, expected) {
   130                         go WaitForAcceptSole(partner, groupkeys);
   131                     }
   132                 }
   133             }
   134             on Timeout {
   135                 do notifyTimeout(expected);
   136                 do sendBeacon;
   137                 go Sole;
   138             }
   139         }
   140     
   141         state WaitForGroupKeysSole timeout=600 (Identity expected) {
   142             on GroupKeys(Identity partner, GroupKeys groupkeys) {
   143                 // UUID changes in between, so we can only check for same address and fpr
   144                 if sameKeyAndAddress(partner, expected) {
   145                     do storeGroupKeys(partner, groupkeys);
   146                     do sendGroupUpdate;
   147                     do renewUUID;
   148                     do notifyAcceptedDeviceAdded(partner);
   149                     go Grouped;
   150                 }
   151             }
   152             on Timeout {
   153                 do notifyTimeout(expected);
   154                 go Sole;
   155             }
   156         }
   157 
   158         state WaitForAcceptSole timeout=600 (Identity expected, GroupKeys groupkeys) {
   159             on HandshakeRejected(Identity partner) {
   160                 do rejectHandshake(partner);
   161                 go Sole;
   162             }
   163             on HandshakeAccepted(Identity partner) {
   164                 // UUID changes in between, so we can only check for same address and fpr
   165                 if sameKeyAndAddress(partner, expected) {
   166                     do acceptHandshake(partner); 
   167                     do storeGroupKeys(partner, groupkeys);
   168                     do sendGroupUpdate;
   169                     do renewUUID;
   170                     do notifyAcceptedDeviceAdded(partner);
   171                     go Grouped;
   172                 }
   173                 go Sole;
   174             }
   175             on Cancel go Sole;
   176             on Timeout {
   177                 do notifyTimeout(expected);
   178                 go Sole;
   179             }
   180         }
   181 
   182         state Grouped end=1 {
   183             on KeyGen
   184                 do sendGroupUpdate;
   185             on CannotDecrypt {
   186                 do sendUpdateRequest;
   187 
   188                 ///// de-activate 3+ de group in test_diphoton
   189                 // do sendBeacon;
   190 
   191                 go GroupWaiting;
   192             }
   193             on UpdateRequest
   194                 do sendGroupUpdate;
   195 
   196             ///// de-activate 3+ de group in test_diphoton
   197             // on Beacon(Identity partner){
   198             //     do sendHandshakeRequest(partner);
   199             //     go GroupedBeaconed(partner);
   200             // }
   201             // on HandshakeRequest(Identity partner) {
   202             //     do sendHandshakeRequest(partner);
   203             //     go HandshakingGrouped(partner);
   204             // }
   205 
   206             on GroupUpdate(Identity partner, IdentityList keys)
   207                 do storeGroupUpdate(partner, keys);
   208         }
   209 
   210         // copy of grouped state, with a timeout to enable fast poling for a minut
   211         state GroupWaiting timeout=60 {
   212             on KeyGen
   213                 do sendGroupUpdate;
   214             on CannotDecrypt {
   215                 do sendUpdateRequest;
   216 
   217                 ///// de-activate 3+ de group in test_diphoton
   218                 // do sendBeacon;
   219             }
   220             on UpdateRequest
   221                 do sendGroupUpdate;
   222 
   223             ///// de-activate 3+ de group in test_diphoton
   224             // on Beacon(Identity partner){
   225             //     do sendHandshakeRequest(partner);
   226             //     go GroupedBeaconed(partner);
   227             // }
   228             // on HandshakeRequest(Identity partner) {
   229             //     do sendHandshakeRequest(partner);
   230             //     go HandshakingGrouped(partner);
   231             // }
   232 
   233             on GroupUpdate(Identity partner, IdentityList keys)
   234                 do storeGroupUpdate(partner, keys);
   235             on Timeout go Grouped;
   236         }
   237 
   238         ///// de-activate 3+ de group in test_diphoton
   239         // state GroupedBeaconed timeout=600 (Identity expected){
   240         //     on KeyGen
   241         //         do sendGroupUpdate;
   242         //     on CannotDecrypt {
   243         //         do sendUpdateRequest;
   244         //         do sendBeacon;
   245         //     }
   246         //     on UpdateRequest
   247         //         do sendGroupUpdate;
   248         //     on Beacon(Identity partner){
   249         //         do sendHandshakeRequest(partner);
   250         //         go GroupedBeaconed(partner);
   251         //     }
   252         //     on HandshakeRequest(Identity partner) {
   253         //         if sameIdentities(partner, expected) {
   254         //             // do nothing, to avoid sending handshake request twice 
   255         //         } else {
   256         //             do sendHandshakeRequest(partner);
   257         //         }
   258         //         go HandshakingGrouped(partner);
   259         //     }
   260         //     on GroupUpdate(Identity partner, IdentityList keys)
   261         //         do storeGroupUpdate(partner, keys);
   262         //     on Timeout go Grouped;
   263         // }
   264 
   265         ///// de-activate 3+ de group in test_diphoton
   266         // state HandshakingGrouped timeout=600 (Identity expected) {
   267         //     // HandshakeRequest from same group are filtered in receive_sync_msg
   268         //     on Init{
   269         //         if keyElectionWon(expected) {
   270         //             do notifyInitAddOtherDevice(partner);
   271         //         } else {
   272         //             do notifyInitMoveOurDevice(partner);
   273         //         }
   274         //     }
   275         //     on HandshakeRejected(Identity partner) {
   276         //         do rejectHandshake(partner);             // stores rejection of partner
   277         //         do sendGroupUpdate;
   278         //         go Grouped;
   279         //     }
   280         //     on HandshakeAccepted(Identity partner) {
   281         //         do acceptHandshake(partner); 
   282         //         do sendGroupUpdate;
   283         //         if keyElectionWon(partner) {
   284         //             do sendGroupKeys(partner);
   285         //             do notifyAcceptedDeviceAdded(partner);
   286         //             go Grouped;
   287         //         }
   288         //         go WaitForGroupKeysGrouped(partner);
   289         //     }
   290         //     on Cancel go Grouped;
   291         //     on GroupKeys(Identity partner, GroupKeys groupkeys) {
   292         //         if keyElectionWon(expected) {
   293         //             // not supposed to receive groupkeys - ignore
   294         //         } else {
   295         //             // UUID changes in between, so we can only check for same address and fpr
   296         //             if sameKeyAndAddress(partner, expected) {
   297         //                 go WaitForAcceptGrouped(partner, groupkeys);
   298         //             }
   299         //         }
   300         //     }
   301         //     on GroupUpdate(Identity partner, IdentityList keys) {
   302         //         do notifyOvertaken(partner);
   303         //         do storeGroupUpdate(partner, keys);
   304         //         go Grouped;
   305         //     }
   306         //     on Timeout {
   307         //         do notifyTimeout(expected);
   308         //         go Grouped;
   309         //     }
   310         // }
   311 
   312         ///// de-activate 3+ de group in test_diphoton
   313         // state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
   314         //     on GroupKeys(Identity partner, GroupKeys groupkeys) {
   315         //         if sameIdentities(partner, expected) {
   316         //             do storeGroupKeys(partner, groupkeys);
   317         //             do sendGroupUpdate;
   318         //             do renewUUID;
   319         //             do notifyAcceptedDeviceMoved(partner);
   320         //             go Grouped;
   321         //         }
   322         //     }
   323         //     on GroupUpdate(Identity partner, IdentityList keys) {
   324         //         do notifyOvertaken(partner);
   325         //         do storeGroupUpdate(partner, keys);
   326         //         go Grouped;
   327         //     }
   328         //     on Timeout {
   329         //         do notifyTimeout(expected);
   330         //         go Grouped;
   331         //     }
   332         // }
   333 
   334         ///// de-activate 3+ de group in test_diphoton
   335         // state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
   336         //     on HandshakeRejected(Identity partner) {
   337         //         do rejectHandshake(partner);
   338         //         do sendGroupUpdate;
   339         //         go Grouped;
   340         //     }
   341         //     on HandshakeAccepted(Identity partner) {
   342         //         if sameIdentities(partner, expected) {
   343         //             do acceptHandshake(partner); 
   344         //             do storeGroupKeys(partner, groupkeys);
   345         //             do sendGroupUpdate;
   346         //             do renewUUID;
   347         //             do notifyAcceptedDeviceMoved(partner);
   348         //         }
   349         //         go Grouped;
   350         //     }
   351         //     on Cancel go Grouped;
   352         //     on GroupUpdate(Identity partner, IdentityList keys) {
   353         //         do notifyOvertaken(partner);
   354         //         do storeGroupUpdate(partner, keys);
   355         //         go Grouped;
   356         //     }
   357         //     on Timeout {
   358         //         do notifyTimeout(expected);
   359         //         go Grouped;
   360         //     }
   361         // }
   362 
   363         tag Init 1;
   364         tag Beacon 2;
   365         tag HandshakeRequest 3;
   366         tag GroupKeys 4;
   367     }
   368 }
   369