// This file is under BSD License 2.0

// Sync protocol for p≡p

// Copyright (c) 2016-2019, p≡p foundation

// Written by Volker Birk

include ./fsm.yml2

protocol Sync 1 {

    // all messages have a timestamp, time out and are removed after timeout

    fsm KeySync 1, threshold=300 {

        version 1, 2;

        state InitState {

            on Init {

                if deviceGrouped

                    go Grouped;

                do newChallengeAndNegotiationBase;

                send Beacon;

                go Sole;

            }

        }

        state Sole timeout=off {

            on Init {

                do showBeingSole;

            }

            on KeyGen {

                send Beacon;

            }

            on CannotDecrypt { // cry baby

                send Beacon;

            }

            on Beacon {

                if sameChallenge {

                    debug > this is our own Beacon; ignore

                }

                else {

                    if weAreOfferer {

                        do useOwnChallenge;

                        send Beacon;

                    }

                    else /* we are requester */ {

                        do openNegotiation;

                        do tellWeAreNotGrouped;

                        // requester is sending NegotiationRequest

                        send NegotiationRequest;

                        do useOwnChallenge;

                    }

                }

            }

            // we get this from another sole device

            on NegotiationRequest {

                if sameChallenge { // challenge accepted

                    if sameNegotiation {

                        // this is our own NegotiationRequest; ignore

                    }

                    else {

                        do storeNegotiation;

                        // offerer is accepting by confirming NegotiationOpen

                        send NegotiationOpen;

                        go HandshakingOfferer;

                    }

                }

            }

            // we get this from an existing device group

            on NegotiationRequestGrouped {

                if sameChallenge { // challenge accepted

                    do storeNegotiation;

                    // offerer is accepting by confirming NegotiationOpen

                    send NegotiationOpen;

                    go HandshakingToJoin;

                }

            }

            on NegotiationOpen if sameNegotiationAndPartner {

                // requester is receiving NegotiationOpen

                do storeNegotiation;

                go HandshakingRequester;

            }

        }

        // handshaking without existing Device group

        state HandshakingOfferer timeout=600 {

            on Init

                do showSoleHandshake;

            // Cancel is Rollback

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Rollback if sameNegotiationAndPartner

                go Sole;

            // Reject is CommitReject

            on Reject {

                send CommitReject;

                do disable;

                go End;

            }

            on CommitReject if sameNegotiationAndPartner {

                do disable;

                go End;

            }

            // Accept means init Phase1Commit

            on Accept {

                do trustThisKey;

                send CommitAcceptOfferer;

                go HandshakingPhase1Offerer;

            }

            // got a CommitAccept from requester

            on CommitAcceptRequester if sameNegotiationAndPartner

                go HandshakingPhase2Offerer;

        }

        // handshaking without existing Device group

        state HandshakingRequester timeout=600 {

            on Init

                do showSoleHandshake;

            // Cancel is Rollback

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Rollback if sameNegotiationAndPartner

                go Sole;

            // Reject is CommitReject

            on Reject {

                send CommitReject;

                do disable;

                go End;

            }

            on CommitReject if sameNegotiationAndPartner {

                do disable;

                go End;

            }

            // Accept means init Phase1Commit

            on Accept {

                do trustThisKey;

                send CommitAcceptRequester;

                go HandshakingPhase1Requester;

            }

            // got a CommitAccept from offerer

            on CommitAcceptOfferer if sameNegotiationAndPartner

                go HandshakingPhase2Requester;

        }

        state HandshakingPhase1Offerer {

            on Rollback if sameNegotiationAndPartner {

                do untrustThisKey;

                go Sole;

            }

            on CommitReject if sameNegotiationAndPartner {

                do untrustThisKey;

                do disable;

                go End;

            }

            on CommitAcceptRequester if sameNegotiationAndPartner {

                go FormingGroupOfferer;

            }

        }

        state HandshakingPhase1Requester {

            on Rollback if sameNegotiationAndPartner {

                do untrustThisKey;

                go Sole;

            }

            on CommitReject if sameNegotiationAndPartner {

                do untrustThisKey;

                do disable;

                go End;

            }

            on CommitAcceptOfferer if sameNegotiationAndPartner {

                go FormingGroupRequester;

            }

        }

        state HandshakingPhase2Offerer {

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Reject {

                send CommitReject;

                do disable;

                go End;

            }

            on Accept {

                do trustThisKey;

                send CommitAcceptOfferer;

                go FormingGroupOfferer;

            }

        }

        state HandshakingPhase2Requester {

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Reject {

                send CommitReject;

                do disable;

                go End;

            }

            on Accept {

                do trustThisKey;

                send CommitAcceptRequester;

                go FormingGroupRequester;

            }

        }

        state FormingGroupOfferer {

            on Init {

                do prepareOwnKeys;

                send OwnKeysOfferer; // we're not grouped yet, this is our own keys

            }

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Rollback

                go Sole;

            on OwnKeysRequester if sameNegotiationAndPartner {

                do saveGroupKeys;

                do receivedKeysAreDefaultKeys;

                do showGroupCreated;

                go Grouped;

            }

        }

        state FormingGroupRequester {

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Rollback

                go Sole;

            on OwnKeysOfferer if sameNegotiationAndPartner {

                do saveGroupKeys;

                do prepareOwnKeys;

                do ownKeysAreDefaultKeys;

                send OwnKeysRequester;

                do showGroupCreated;

                go Grouped;

            }

        }

        state Grouped timeout=off {

            on Init {

                do newChallengeAndNegotiationBase;

                do showBeingInGroup;

            }

            on GroupKeysUpdate if fromGroupMember // double check

                do saveGroupKeys;

            on KeyGen {

                do prepareOwnKeys;

                send GroupKeysUpdate;

            }

            on Beacon {

                do openNegotiation;

                do tellWeAreGrouped;

                send NegotiationRequestGrouped;

                do useOwnChallenge;

            }

            on NegotiationOpen if sameNegotiationAndPartner {

                do storeNegotiation;

                do useThisKey;

                send GroupHandshake;

                go HandshakingGrouped;

            }

            on GroupHandshake {

                do storeNegotiation;

                do storeThisKey;

                go HandshakingGrouped;

            }

            on GroupTrustThisKey if fromGroupMember // double check

                do trustThisKey;

            on GroupKeyResetRequired {

                do ledGroupKeyReset;

                send GroupKeyReset;

            }

            // this is for a leaving group member

            on GroupKeyResetRequiredAndDisable {

                send InitUnledGroupKeyReset;

                go DisableOnInitUnledGroupKeyReset;

            }

            on InitUnledGroupKeyReset {

                // unled group key reset; new group keys will be elected

                do unledGroupKeyReset;

                send GroupKeyReset;

            }

            on GroupKeyReset if fromGroupMember { // double check

                do saveGroupKeys;

                if isLedGroupKeyReset {

                    // led group key reset is executed without questions

                    do receivedKeysAreDefaultKeys;

                }

                else {

                    // unled group key reset; election takes place

                    if keyElectionWon {

                        // this is already the case:

                        // do ownKeysAreDefaultKeys;

                    }

                    else {

                        do receivedKeysAreDefaultKeys;

                    }

                }

            }

        }

        state DisableOnInitUnledGroupKeyReset {

            on InitUnledGroupKeyReset

                do disable;

        }

        // sole device handshaking with group

        state HandshakingToJoin {

            on Init

                do showJoinGroupHandshake;

            // Cancel is Rollback

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Rollback if sameNegotiationAndPartner

                go Sole;

            // Reject is CommitReject

            on Reject {

                send CommitReject;

                do disable;

                go End;

            }

            on CommitAcceptForGroup if sameNegotiationAndPartner

                go HandshakingToJoinPhase2;

            on CommitReject if sameNegotiationAndPartner {

                do disable;

                go End;

            }

            // Accept is Phase1Commit

            on Accept {

                do trustThisKey;

                send CommitAccept;

                go HandshakingToJoinPhase1;

            }

        }

        state HandshakingToJoinPhase1 {

            on Rollback if sameNegotiationAndPartner

                go Sole;

            on CommitReject if sameNegotiationAndPartner {

                do disable;

                go End;

            }

            on CommitAcceptForGroup if sameNegotiationAndPartner

                go JoiningGroup;

        }

        state HandshakingToJoinPhase2 {

            on Cancel {

                send Rollback;

                go Sole;

            }

            on Reject {

                send CommitReject;

                do disable;

                go End;

            }

            on Accept {

                do trustThisKey;

                send CommitAccept;

                go JoiningGroup;

            }

        }

        state JoiningGroup {

            on GroupKeysForNewMember if sameNegotiationAndPartner {

                do saveGroupKeys;

                do receivedKeysAreDefaultKeys;

                do prepareOwnKeys;

                send GroupKeysAndClose;

                do showDeviceAdded;

                go Grouped;

            }

        }

        state HandshakingGrouped {

            on Init

                do showGroupedHandshake;

            // Cancel is Rollback

            on Cancel {

                send Rollback;

                go Grouped;

            }

            on Rollback if sameNegotiationAndPartner

                go Grouped;

            // Reject is CommitReject

            on Reject {

                send CommitReject;

                go Grouped;

            }

            on CommitReject if sameNegotiationAndPartner

                go Grouped;

            // Accept is Phase1Commit

            on Accept {

                do trustThisKey;

                go HandshakingGroupedPhase1;

            }

            on CommitAccept if sameNegotiationAndPartner

                go HandshakingGroupedPhase2;

            on GroupTrustThisKey if fromGroupMember { // double check

                do trustThisKey;

                if sameNegotiation

                    go Grouped;

            }

            on GroupKeysUpdate if fromGroupMember // double check

                do saveGroupKeys;

        }

        state HandshakingGroupedPhase1 {

            on Init {

                send GroupTrustThisKey;

                send CommitAcceptForGroup;

            }

            on Rollback if sameNegotiationAndPartner

                go Grouped;

            on CommitReject if sameNegotiationAndPartner

                go Grouped;

            on CommitAccept if sameNegotiationAndPartner {

                do prepareOwnKeys;

                send GroupKeysForNewMember;

                do showDeviceAccepted;

                go Grouped;

            }

            on GroupTrustThisKey if fromGroupMember // double check

                do trustThisKey;

            on GroupKeysUpdate if fromGroupMember // double check

                do saveGroupKeys;

            on GroupKeysAndClose if fromGroupMember { // double check

                do saveGroupKeys;

                go Grouped;

            }

        }

        state HandshakingGroupedPhase2 {

            on Cancel {

                send Rollback;

                go Grouped;

            }

            on Reject {

                send CommitReject;

                go Grouped;

            }

            on Accept {

                do trustThisKey;

                send GroupTrustThisKey;

                do prepareOwnKeys;

                send GroupKeysForNewMember;

                do showDeviceAccepted;

                go Grouped;

            }

            on GroupTrustThisKey if fromGroupMember // double check

                do trustThisKey;

            on GroupKeysUpdate if fromGroupMember // double check

                do saveGroupKeys;

            on GroupKeysAndClose if fromGroupMember { // double check

                do saveGroupKeys;

                go Grouped;

            }

        }

        external Accept 129;

        external Reject 130;

        external Cancel 131;

        // beacons are always broadcasted

        message Beacon 2, type=broadcast, security=unencrypted {

            field TID challenge;

            auto Version version;

        }

        message NegotiationRequest 3, security=untrusted {

            field TID challenge;

            auto Version version;

            field TID negotiation;

            field bool is_group;

        }

        message NegotiationOpen 4, security=untrusted {

            auto Version version;

            field TID negotiation;

        }

        message Rollback 5, security=untrusted {

            field TID negotiation;

        }

        message CommitReject 6, security=untrusted {

            field TID negotiation;

        }

        message CommitAcceptOfferer 7, security=untrusted {

            field TID negotiation;

        }

        message CommitAcceptRequester 8, security=untrusted {

            field TID negotiation;

        }

        message CommitAccept 9, security=untrusted {

            field TID negotiation;

        }

        message CommitAcceptForGroup 10, security=untrusted {

            field TID negotiation;

        }

        // default: security=truste

        // messages are only accepted when coming from the device group

        message GroupTrustThisKey 11 {

            field Hash key;

            field TID negotiation;

        }

        // trust in future

        message GroupKeysForNewMember 12, security=attach_own_keys_for_new_member {

            field IdentityList ownIdentities;

        }

        message GroupKeysAndClose 13, security=attach_own_keys_for_new_member {

            field IdentityList ownIdentities;

        }

        message OwnKeysOfferer 14, security=attach_own_keys_for_new_member {

            field IdentityList ownIdentities;

        }

        message OwnKeysRequester 15, security=attach_own_keys_for_new_member {

            field IdentityList ownIdentities;

        }

        // grouped handshake

        message NegotiationRequestGrouped 16, security=untrusted {

            field TID challenge;

            auto Version version;

            field TID negotiation;

            field bool is_group;

        }

        message GroupHandshake 17 {

            field TID negotiation;

            field Hash key;

        }

        // update group

        message GroupKeysUpdate 18, security=attach_own_keys_for_group {

            field IdentityList ownIdentities;

        }

        // initiate unled group key reset

        message InitUnledGroupKeyReset 19 {

        }

        message GroupKeyReset 20, security=attach_own_keys_for_group {

            field TID challenge;

            // set this flag for led group key reset; delivered group keys will

            // be accepted by all group members; if not set group keys will be

            // elected

            field bool led;

            field IdentityList ownIdentities;

        }

    }

}