You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
354 lines
12 KiB
354 lines
12 KiB
// This file is under GNU General Public License 3.0
|
|
// see LICENSE.txt
|
|
|
|
// DeviceGroup protocol for p≡p
|
|
|
|
// Copyleft (c) 2016, p≡p foundation
|
|
|
|
// Written by Volker Birk
|
|
|
|
include ./fsm.yml2
|
|
|
|
protocol DeviceGroup {
|
|
// all messages have a timestamp, time out and are removed after timeout
|
|
|
|
broadcast sendBeacon;
|
|
broadcast sendGroupUpdate;
|
|
broadcast sendUpdateRequest;
|
|
unencrypted sendBeacon;
|
|
|
|
fsm DeviceState filename=sync {
|
|
condition deviceGrouped();
|
|
condition keyElectionWon(Identity partner);
|
|
condition sameIdentities(Identity a, Identity b);
|
|
condition sameKeyAndAddress(Identity a, Identity b);
|
|
|
|
state InitState {
|
|
on Init {
|
|
if deviceGrouped()
|
|
go Grouped;
|
|
go Sole;
|
|
}
|
|
}
|
|
|
|
state Sole end=1 {
|
|
on KeyGen {
|
|
do sendBeacon;
|
|
go SoleWaiting;
|
|
}
|
|
on CannotDecrypt {
|
|
do sendBeacon;
|
|
go SoleWaiting;
|
|
}
|
|
on Beacon(Identity partner){
|
|
do sendHandshakeRequest(partner);
|
|
go SoleBeaconed(partner);
|
|
}
|
|
on HandshakeRequest(Identity partner) {
|
|
do sendHandshakeRequest(partner);
|
|
go HandshakingSole(partner);
|
|
}
|
|
}
|
|
|
|
// copy of sole state with a timeout to enable fast polling for a second
|
|
// TODO use more YSLT power here (substates ?)
|
|
state SoleWaiting timeout=60 {
|
|
on KeyGen {
|
|
do sendBeacon;
|
|
}
|
|
on CannotDecrypt {
|
|
do sendBeacon;
|
|
}
|
|
on Beacon(Identity partner){
|
|
do sendHandshakeRequest(partner);
|
|
go SoleBeaconed(partner);
|
|
}
|
|
on HandshakeRequest(Identity partner) {
|
|
do sendHandshakeRequest(partner);
|
|
go HandshakingSole(partner);
|
|
}
|
|
on Timeout go Sole;
|
|
}
|
|
|
|
state SoleBeaconed timeout=600 (Identity expected) {
|
|
on KeyGen{
|
|
do sendBeacon;
|
|
go Sole;
|
|
}
|
|
on CannotDecrypt{
|
|
do sendBeacon;
|
|
go Sole;
|
|
}
|
|
on Beacon(Identity partner) {
|
|
do sendHandshakeRequest(partner);
|
|
go SoleBeaconed(partner);
|
|
}
|
|
on HandshakeRequest(Identity partner) {
|
|
if sameIdentities(partner, expected) {
|
|
// do nothing, to avoid sending handshake request twice
|
|
} else {
|
|
do sendHandshakeRequest(partner);
|
|
}
|
|
go HandshakingSole(partner);
|
|
}
|
|
on Timeout go Sole;
|
|
}
|
|
|
|
state HandshakingSole timeout=600 (Identity expected) {
|
|
on Init{
|
|
if keyElectionWon(expected) {
|
|
do notifyInitFormGroup(expected);
|
|
} else {
|
|
do notifyInitAddOurDevice(expected);
|
|
}
|
|
}
|
|
on HandshakeRejected(Identity partner) {
|
|
do rejectHandshake(partner);
|
|
go Sole;
|
|
}
|
|
on HandshakeAccepted(Identity partner) {
|
|
if sameIdentities(partner, expected) {
|
|
do acceptHandshake(partner);
|
|
if keyElectionWon(partner) {
|
|
do makeGroup;
|
|
do sendGroupKeys(partner);
|
|
do renewUUID;
|
|
do notifyAcceptedGroupCreated(partner);
|
|
go Grouped;
|
|
}
|
|
go WaitForGroupKeysSole(partner);
|
|
}
|
|
go Sole;
|
|
}
|
|
on Cancel go Sole;
|
|
on GroupKeys(Identity partner, GroupKeys groupkeys) {
|
|
if keyElectionWon(expected) {
|
|
// not supposed to receive groupkeys - ignore
|
|
} else {
|
|
// UUID changes in between, so we can only check for same address and fpr
|
|
if sameKeyAndAddress(partner, expected) {
|
|
go WaitForAcceptSole(partner, groupkeys);
|
|
}
|
|
}
|
|
}
|
|
on Timeout {
|
|
do notifyTimeout(expected);
|
|
do sendBeacon;
|
|
go Sole;
|
|
}
|
|
}
|
|
|
|
state WaitForGroupKeysSole timeout=600 (Identity expected) {
|
|
on GroupKeys(Identity partner, GroupKeys groupkeys) {
|
|
// UUID changes in between, so we can only check for same address and fpr
|
|
if sameKeyAndAddress(partner, expected) {
|
|
do storeGroupKeys(partner, groupkeys);
|
|
do sendGroupUpdate;
|
|
do renewUUID;
|
|
do notifyAcceptedDeviceAdded(partner);
|
|
go Grouped;
|
|
}
|
|
}
|
|
on Timeout {
|
|
do notifyTimeout(expected);
|
|
go Sole;
|
|
}
|
|
}
|
|
|
|
state WaitForAcceptSole timeout=600 (Identity expected, GroupKeys groupkeys) {
|
|
on HandshakeRejected(Identity partner) {
|
|
do rejectHandshake(partner);
|
|
go Sole;
|
|
}
|
|
on HandshakeAccepted(Identity partner) {
|
|
// UUID changes in between, so we can only check for same address and fpr
|
|
if sameKeyAndAddress(partner, expected) {
|
|
do acceptHandshake(partner);
|
|
do storeGroupKeys(partner, groupkeys);
|
|
do sendGroupUpdate;
|
|
do renewUUID;
|
|
do notifyAcceptedDeviceAdded(partner);
|
|
go Grouped;
|
|
}
|
|
go Sole;
|
|
}
|
|
on Cancel go Sole;
|
|
on Timeout {
|
|
do notifyTimeout(expected);
|
|
go Sole;
|
|
}
|
|
}
|
|
|
|
state Grouped end=1 {
|
|
on KeyGen
|
|
do sendGroupUpdate;
|
|
on CannotDecrypt {
|
|
do sendUpdateRequest;
|
|
do sendBeacon;
|
|
go GroupWaiting;
|
|
}
|
|
on UpdateRequest
|
|
do sendGroupUpdate;
|
|
on Beacon(Identity partner){
|
|
do sendHandshakeRequest(partner);
|
|
go GroupedBeaconed(partner);
|
|
}
|
|
on HandshakeRequest(Identity partner) {
|
|
do sendHandshakeRequest(partner);
|
|
go HandshakingGrouped(partner);
|
|
}
|
|
on GroupUpdate(Identity partner, IdentityList keys)
|
|
do storeGroupUpdate(partner, keys);
|
|
}
|
|
|
|
// copy of grouped state, with a timeout to enable fast poling for a minut
|
|
state GroupWaiting timeout=60 {
|
|
on KeyGen
|
|
do sendGroupUpdate;
|
|
on CannotDecrypt {
|
|
do sendUpdateRequest;
|
|
do sendBeacon;
|
|
}
|
|
on UpdateRequest
|
|
do sendGroupUpdate;
|
|
on Beacon(Identity partner){
|
|
do sendHandshakeRequest(partner);
|
|
go GroupedBeaconed(partner);
|
|
}
|
|
on HandshakeRequest(Identity partner) {
|
|
do sendHandshakeRequest(partner);
|
|
go HandshakingGrouped(partner);
|
|
}
|
|
on GroupUpdate(Identity partner, IdentityList keys)
|
|
do storeGroupUpdate(partner, keys);
|
|
on Timeout go Grouped;
|
|
}
|
|
|
|
state GroupedBeaconed timeout=600 (Identity expected){
|
|
on KeyGen
|
|
do sendGroupUpdate;
|
|
on CannotDecrypt {
|
|
do sendUpdateRequest;
|
|
do sendBeacon;
|
|
}
|
|
on UpdateRequest
|
|
do sendGroupUpdate;
|
|
on Beacon(Identity partner){
|
|
do sendHandshakeRequest(partner);
|
|
go GroupedBeaconed(partner);
|
|
}
|
|
on HandshakeRequest(Identity partner) {
|
|
if sameIdentities(partner, expected) {
|
|
// do nothing, to avoid sending handshake request twice
|
|
} else {
|
|
do sendHandshakeRequest(partner);
|
|
}
|
|
go HandshakingGrouped(partner);
|
|
}
|
|
on GroupUpdate(Identity partner, IdentityList keys)
|
|
do storeGroupUpdate(partner, keys);
|
|
on Timeout go Grouped;
|
|
}
|
|
|
|
state HandshakingGrouped timeout=600 (Identity expected) {
|
|
// HandshakeRequest from same group are filtered in receive_sync_msg
|
|
on Init{
|
|
if keyElectionWon(expected) {
|
|
do notifyInitAddOtherDevice(partner);
|
|
} else {
|
|
do notifyInitMoveOurDevice(partner);
|
|
}
|
|
}
|
|
on HandshakeRejected(Identity partner) {
|
|
do rejectHandshake(partner); // stores rejection of partner
|
|
do sendGroupUpdate;
|
|
go Grouped;
|
|
}
|
|
on HandshakeAccepted(Identity partner) {
|
|
do acceptHandshake(partner);
|
|
do sendGroupUpdate;
|
|
if keyElectionWon(partner) {
|
|
do sendGroupKeys(partner);
|
|
do notifyAcceptedDeviceAdded(partner);
|
|
go Grouped;
|
|
}
|
|
go WaitForGroupKeysGrouped(partner);
|
|
}
|
|
on Cancel go Grouped;
|
|
on GroupKeys(Identity partner, GroupKeys groupkeys) {
|
|
if keyElectionWon(expected) {
|
|
// not supposed to receive groupkeys - ignore
|
|
} else {
|
|
// UUID changes in between, so we can only check for same address and fpr
|
|
if sameKeyAndAddress(partner, expected) {
|
|
go WaitForAcceptGrouped(partner, groupkeys);
|
|
}
|
|
}
|
|
}
|
|
on GroupUpdate(Identity partner, IdentityList keys) {
|
|
do notifyOvertaken(partner);
|
|
do storeGroupUpdate(partner, keys);
|
|
go Grouped;
|
|
}
|
|
on Timeout {
|
|
do notifyTimeout(expected);
|
|
go Grouped;
|
|
}
|
|
}
|
|
|
|
state WaitForGroupKeysGrouped timeout=600 (Identity expected) {
|
|
on GroupKeys(Identity partner, GroupKeys groupkeys) {
|
|
if sameIdentities(partner, expected) {
|
|
do storeGroupKeys(partner, groupkeys);
|
|
do sendGroupUpdate;
|
|
do renewUUID;
|
|
do notifyAcceptedDeviceMoved(partner);
|
|
go Grouped;
|
|
}
|
|
}
|
|
on GroupUpdate(Identity partner, IdentityList keys) {
|
|
do notifyOvertaken(partner);
|
|
do storeGroupUpdate(partner, keys);
|
|
go Grouped;
|
|
}
|
|
on Timeout {
|
|
do notifyTimeout(expected);
|
|
go Grouped;
|
|
}
|
|
}
|
|
|
|
state WaitForAcceptGrouped timeout=600 (Identity expected, GroupKeys groupkeys) {
|
|
on HandshakeRejected(Identity partner) {
|
|
do rejectHandshake(partner);
|
|
do sendGroupUpdate;
|
|
go Grouped;
|
|
}
|
|
on HandshakeAccepted(Identity partner) {
|
|
if sameIdentities(partner, expected) {
|
|
do acceptHandshake(partner);
|
|
do storeGroupKeys(partner, groupkeys);
|
|
do sendGroupUpdate;
|
|
do renewUUID;
|
|
do notifyAcceptedDeviceMoved(partner);
|
|
}
|
|
go Grouped;
|
|
}
|
|
on Cancel go Grouped;
|
|
on GroupUpdate(Identity partner, IdentityList keys) {
|
|
do notifyOvertaken(partner);
|
|
do storeGroupUpdate(partner, keys);
|
|
go Grouped;
|
|
}
|
|
on Timeout {
|
|
do notifyTimeout(expected);
|
|
go Grouped;
|
|
}
|
|
}
|
|
|
|
tag Init 1;
|
|
tag Beacon 2;
|
|
tag HandshakeRequest 3;
|
|
tag GroupKeys 4;
|
|
}
|
|
}
|
|
|