Audit Report: Secure Scuttlebutt Partial Replication and Fusion Identity
Authors: Justin Regele (Arxum Path Security GmbH), Jan Winkelmann
Introduction
This reports documents the findings from the audit of the Secure Scuttlebutt Partial Replication and Fusion Identity specifications. While we did not find any immediate security concerns, we do provide suggestions below on areas that could be improved. Our research also included a formal analysis, i.e. a mathematical modeling, of the Fusion Identity protocol, where we found that the security properties of the protocol hold under the assumptions of our model. We do note that our model is our interpretation of the protocol, and therefore the security of a particular implementation of the protocol will be conditional to its adherence to our model.
The report begins with a summary, describing the protocols, our methodology, and a high level overview of our suggestions. This is followed by a short section on partial replication in which we discuss the work performed during this phase of the audit. The remainder of the report documents in depth our formal analysis of the Fusion Identity protocol. We discuss at a high level how we modelled the protocol using the Tamarin Prover, and then document our Rules and Lemmas individually so that the reader can understand our intentions behind the code associated with this report.
This section is then followed by the Issues and Suggestions, and we conclude with our thoughts on further work.
Summary / Gist
We report on our analysis of two new subcomponents in the Secure Scuttlebutt ecosystem: The Fusion ID mechanism and the partial replication protocol. The specification documents in scope are:
Meta Feeds are a core piece of the partial replication protocol designed by the SSB NGI Pointer team. It describes a standard way to build hierarchical feeds, where there is a single root feed and multiple subfeeds. These subfeeds can be used for different purposes, including maintaining indexes of messages. For example, One feed could be the main feed where messages are posted as they are in the current version of Scuttlebutt, and additionally there could be a feed that posts references to all messages that are of type “post”. This would be done with the goal of quickly finding all post messages by that user.
The Fusion ID protocol is a way to join multiple feeds into a single logical identity. The main motivation here is that in Scuttlebutt, users have multiple devices, but each device must have its own Scuttlebutt feed due to synchronization issues. Fusion IDs are an attempt to mitigate the impact on the user experience this technical limitation has.
The partial replication protocol was assessed through the means of a manual review of the specification, as well as clarifying conversations with the authors of the specification.
The Fusion ID protocol was reviewed more rigorously, using formal methods, i.e. a sound mathematical model. Specifically, we use the Tamarin prover to model the protocol and the security properties we expect to hold.
Additionally, an early review of parts of the Rooms 2 Specification was performed in pull requests #17 and #18. Some changes were recommended and quickly applied to the specification. In particular, signed strings should include a reference to the rooms protocol in order to avoid the possiblity of interactions with other protocols. More importantly, however, is that the authenticating signatures should contain the nonces of both parties, in order to guarantee liveness of both parties. Since the nature of this work was an early design consultation, we do not mark the recommended changes as issues in this report.
We did not find immediate security issues in the security components in scope. However, we noticed that in several parts, the specification was not very precise and left room for interpretation. In the context of our work we were able to get clarifications of what the intended protocol mechanisms were, and used these in our modeling. Other parties will however implement their own, possibly different, interpretation of the specification, which may lead to incompatibility or invalidation of our security analysis (see Issue A).
Additionally, we suggest further development of the protocol by adding a protocol extension for improving the trust placed in redirects (see Suggestion A). Furthermore, we advocate making recommendations for secure storage of the keys used in the protocol, and clearly specifying which values should be considered secret (see Suggestion B).
The formal analysis however showed that, based on the assumptions made in the model, the protocol is secure according to the security properties we defined. The two central security properties are fusion secret secrecy and membership soundness, which, besides some additional ones, are described in the Lemmas section.
With regard to the general approach to security, however, we do have to note two shortcomings. Firstly, only the transport encryption protocol provides forward secrecy (see Issue B). This is a security property that should be provided by a modern communication protocol. Secondly, the storage of private keys lacks a description of security best practices (see Suggestion B).
Partial Replication
The partial replication specification was reviewed manually and questions were discussed with the authors. The feed format for Meta feeds was discussed and the Bendy Butt format was agreed upon as the best suited for the protocol.
When discussing the derivation of signing keys of the different feeds, it was recommended that a salt should be used to derive the signing keys, e.g. using HMAC. This would allow a deterministic derivation of all signing keys from a single secret seed. It was recommended that 32 bytes was sufficient input for the seed. Additionally, 32 bytes was agreed upon for the size of the nonce, and that random data could be used for the nonce instead of a timestamp, since collisions on random 256-bit values are negligibly rare.
In the design of subprotocols that make use of signing, it is important to keep the domains of SSB messages signing and the different subprotocols separated. We found that the team has done a good job doing this.
The trust model for auditing claims was discussed. One potential concern for the system was regarding incentives for members of the network to perform audits of claims. In situations where all of the users are using thing clients, auditing claims would not be feasible, as auditing requires resources not available on mobile devices. This could result in centralization as specific nodes would handle all the auditing, and therefore trust would be centralized to these nodes. This is more of a concern regarding decentralization than the security of the protocol. However, if decentralization itself is considered a security property for the network, then the centralizating of auditing nodes could pose a security concern. If partial replication is dependent on a small number of nodes, the trustworthiness of these nodes (i.e. have they been compromised) would affect the trustworthiness of the partial replication protocol. Despite the emphasis on decentralization, the existence of pubs demonstrates that some centralization is useful for the ecosystem’s usability. It was concluded that as long as auditing nodes were not reduced to a single point of failure, nodes coming to consensus on auditing claims would work securely much as they do in a setting involving a blockchain.
Fusion Identity Protocol
In this section we take a closer look at the Fusion ID protocol. First we describe the features and the protocol flow. In subsection Audit we present the results of our manual review. In Formal Analysis we first provide an introduction to the tool we used, then explain how we modelled the protocol and security properties, go into limitations of the system and finally present the results.
Description
The protocol flow is described in the following sequence diagram:
The source code for this diagram can be found in Appendix A.
There are several methodologies for rigorously analyzing the security of a protocol. When it comes to cryptographic protocols, the computational model is usually considered the strongest. However, performing analyses in this model is very complex, and focuses more on the security of the cryptographic components, rather than logic errors.
Formal methods are an approach that have its origins in type theory and have been used for verifying program correctness for a long time. Since then, theories for many cryptographic algorithms have been introduced, allowing to model cryptographic protocols as well.
In this work we use the Tamarin prover. It provides theories for many common cryptographic primitives and reasons about network flow and attacker knowledge. The source code of the model we developed can be found in Appendix B.
In our analysis, we showed that all security properties we formulated hold for the modelled protocol.
The rest of this section is structured as follows: First we give a brief introduction to the way protocols and security properties are modelled in Tamarin. Then we provide an overview over the way the Fusion ID protocol is modelled, and then into how the security properties we aim for are modelled. We conclude with a brief section that discuss the limitations of this approach.
Modelling in Tamarin
The fundamental concept is as follows: The modeller describes rules that modify the current state of the “modelled world”. That world is modelled as a collection of so called facts, which are atomic state objects such as UserIsInvited(uid, fid) to denote that the user with id uid is invited to fusion id fid.
A rule can change that world by consuming old and producing new facts. For example, there could be a rule where the UserIsInvited fact is consumed and replaced with a UserHasAccepted fact.
Tamarin provides some special facts that help with modelling cryptographic protocols. Firstly, there is the Fr (for fresh) fact, which is used to create new random values. Secondly, there are the In and Out facts, which are used to model both network interaction and attacker knowledge; a rule can consume a fact In(msg), which represents receiving a message, and produce an Out(msg) fact, which represents sending one. The network model of Tamarin is simple: It assumes that all that is sent to the network is received by the adversary, which is then able to provide it as input to any rule consuming an In fact (assuming the rule is fulfilled).
Rules usually consume and produce more than one fact, and the data that is contained in these facts is usually related. For example, a rule can consume a signed message, and the key used for signing must match a that of a registered user. This means, that rules are used to model the correct flow of the protocol, but as soon as the attacker learns a secret, they can also use it for signing, encrypting or decrypting, and then use values they learned from this as well.
Each sequence of application of rules will lead to a different collection of facts. In Tamarin, security properties are defined by declaring that in all valid applications of rules, a certain invariant holds. In order to formulate these statements, we need another class of facts. To not confuse our terminology too much, lets call the facts from earlies state facts (because they describe the state of the model). This new class of facts is called action facts. Rules can also specify to produce those, but these can not be consumed later on. Instead, they are written to a trace, which describes the sequence of all rules that have been applied.
The security properties are then formulated as lemmas, which are logic statements over predicates, quantified over all possible traces - either formulated as “for all” or “there does not exist”. There is another feature that uses this kind of statement: restrictions. These can be used to limit the traces that are being analyzed. In our model one example we use these for is to prevent parties from inviting themselves.
As a side note: there also are lemmas of the form “there exists a trace”. This is used for sanity-checking the model, i.e. to ensure that there even exists a way for the protocol to terminate as intended.
Rules
Here we document the rules in our Model. We begin with the first rules in more detail, explaining the syntax of each rule, along with its intention. Later we move onto only explaining the rule’s intention, as the reader comes to understand Tamarin’s syntax.
Register Device
The AARegisterDevice Rule is named because Tamarin uses alphabetic sorting to choose cases to search. We found that by naming this rule with a prepended AA, this solved problems of Tamarin becoming lost and getting caught in endless loops during automated proving. The defined rule is as follows:
rule AARegister_Device:
let
devVK = pk(~devSK)
in
[ Fr(~devSK) ]
--[ NewDevice(devVK, ~devSK) ]->
[
!Device(devVK),
Out(devVK)
]
The rule defines a device, which uses pattern matching to pair the device’s signing key devSK with the device’s verification key devVK. Fr(~devSK) instructs Tamarin to generate a fresh signing key for this device as an input fact. The action fact NewDevice(devVK, ~devSK) registers this new Device. !Device(devVK) in the output facts means the device is now available in the system and is persistent and will not disappear when consumed by other rules (indicated by the !). Out(devVK) means that the device’s verification key is now publicly available.
Lose Device
rule Lose_Device:
let
devVK = pk(devSK)
in
[ !Device(devVK) ]
--[ LoseDevice(devVK) ]->
[ !DeviceLost(devVK)
, Out(devSK) ]
The Lose_Device rule takes in a Device, and outputs a DeviceLost fact for that device VK, along with the SK for the device. The Action fact for this rule is simply LoseDevice.
Initialize FusionID
This rule models the initialization of a Fusion Identity. Its inputs are:
- a fid, which is the public key for a freshly generated fusion secret
- a device along with its keypair
- a signed init message containing the device’s verification key and the fid, signed with the device’s signing key
In the action traces, the rule models the following states changes:
- the fusion ID is initialized
- the device creating the fusion id is added to the fusion id
- the device creating the fusion id learns about the fusion id
- the device creating the fusion id learns the fusion secret
The rules output states appear similar to the state changes in the action traces. State_IsInFusionID and State_KnowsFusionID appear similar to StateChange_AddToFusionID and StateChange_LearnAboutFusionID. However, the distinction is important for Tamarin as they are different types of facts. Within the trace are action facts, which indicate a change, whereas the facts in the output indicate the result.
Receive Init Message
ReceiveInitMsg takes an initor (initiator) and a rcpt (recipient), and models another device on the network observing that a the fusion id has been intialized. State_Change_AddToFusionID(rcptVK, fid, initorVK) means that rcptVK now knows that the initorVK is in fusion id fid.
Send Invitation
SendInvite models the sending of an invite to join the fusion identity. The input requirements are that the invitor knows the fusion identity and is a part of it. The invitee is an arbitrary input. The state changes are that the invite has been sent and that the invitor knows that the invitee has been invited.
Receive Invitation
Models the reception of an invite. The rule requires a fid, invitor, invitee and recipient. The NotEqual restriction is used to ensure that the invitee is not the same as the invitor. The output of this is that the recipient is aware that the invitee has been invited by the invitor. The recipient and the invitee can be separate entities as everyone on the network will see the invitation.
Accept Invitation
This rule specifies that if the invitee was the same as the recipient in ReceiveInvite, then the invite is accepted. The invitee sets their state to being invited and more importantly Consents to the FusionID. This rule outputs an accept message.
Receive Accept
This rule is similar to ReceiveInvitation, in that it models how all device’s on the network will observe the message. We have commented out the verification of the accept messages signature to improve the working of Tamarin. This could be a potential area for future research. The output of this rule is that the recipient knows that the invitee has accepted the invite by the invitor.
Send Entrust
When an invitor knows that an invitee has consented to their invitation, is in the fusion ID and knows the fusion secret, the fusion secret is encrypted and sent to the invitee. A State Change is also put on the trace, marking that the invitor knows that the invitee has been entrusted.
Send Proof of Key
This rule processes the encrypted entrust message. It also defines a Proof of Key message, containing an inner and outer signed message. The inner message is signed with the fusion secret to prove knowledge of the key. The signed inner message is then included in the outer message, with is signed with the invitee’s signing key. The state changes in this rule occur for the invitee’s state, where the invitee adds itself to the fusion identity and learns the fusion secret.
Receive Proof of Key
The proof of key message is taken as input. Because we use pattern matching and recreate the same Proof of Key message in the prelude to ReceiveProofOfKey as was done in SendProofOfKey, the message is guaranteed to be signed correctly. The recipient stores receipt of the proof of key in their internal state. This is the final step in all recipients knowing that the invitee is now in the fusion identity.
Send Tombstone
SendTombstone is a simple rule that outputs a signed tombstone message, and sets the internal state of the device sending the tombstone message (the tomber) that the fusion identity has been tombstoned.
Receive Tombstone
The recipient will set the fusion identity to be tombstoned if the sender of the message is in the fusion identity.
Send Redirect
A signed redirect message is output if the sender is in both the old and new fusion identities and the old fusion identity is tombstoned.
Receive Redirect
A redirect message with a valid signature is received if the sender is in both the old and new fusion identities.
Attest Redirect
An attestation of either “accept” or “reject” is modelled. We decided to not model the null case as it was ambiguous. A signed attestation message is output, along with a state change for the attestor of either “accept” or “reject”.
Restrictions
dont_invite_members
This restriction prevents tamarin from sending an invite to an invitee if that invitee has already been added to the fusion identity in the invitor’s state.
enforce_not_equal
This restriction prevents two entities from being equal. It is used to ensure that the invitee is not the invitor in ReceiveInvite.
receive_init_only_once
This restriction prevents receiving an init message multiple times. This was necesary to prevent Tamarin from getting caught in endless loops
Lemmas
Fusion Secret Secrecy
Another central security propery of the protocol is that the fusion secret remains secret, as long as none of the members of the fusion id remain honest, i.e. don’t go rogue, lose their device or otherwise leak the key to the adversary.
Roughly, we say that under no circumstances there is a Fusion ID and member thereof, where the adversary knows the key without any member of the Fusion ID losing their device. In Tamarin syntax and using our action facts, this is encoded as follows:
lemma fusion_secret_secrecy:
// there does not exist
"not (Ex initor fid fusionSecret #init #learn.
// a fusion id `fid` and matching secret `fusionSecret`
InitFusionID(fid, initor, fusionSecret) @ #init &
// where the adversary knows the secret
K(fusionSecret) @ #learn &
// and neither the initiator
not (Ex #lose. LoseDevice(initor) @ #lose) &
// nor a party the key was legally entrusted to lost their keys
not (Ex anyEntruster anyEntrustee #entrust #lose.
EntrustSent(fid, anyEntruster, anyEntrustee) @ #entrust &
LoseDevice(anyEntrustee) @ #lose
)
)"
Membership Soundness
A core security property is that nodes don’t get confused about which parties are in the Fusion ID. Only those invited by someone who already is a member should be considered candidates. This lemma proves that for all members that have been added by invitation, there exists someone who was a member before who invited them, or the one they thought they received the invitation from lost their device before. Note that there is one more case: After attaining the fusion secret, the attacker could create another sockpuppet and perform valid invitations from that peer. This rather complex security statement is modelled as follows:
lemma membership_soundness:
"All Invee Invr fid #added.
(
StateChange_AddToFusionID(Invee, fid, Invee) @ #added &
AddedByInvitation(Invr) @ #added
) ==> (
// case 1: proper invitation flow
(Ex #invrAdded #invite.
StateChange_AddToFusionID(Invr, fid, Invr) @ #invrAdded &
InviteSent(fid, Invr, Invee) @ #invite &
#invite < #added
) |
// case 2: the attacker takes over a member
(Ex fusionSecret #lose #learn.
LoseDevice(Invr) @ #lose &
StateChange_LearnFusionSecret(Invr, fid, fusionSecret) @ #learn &
#learn < #added
) |
// case 3: the attacker stole a device that was entrusted the secret and steals some other device to send the entrust from
(Ex anyone secretHolder #invrLose #fusionSecretLose #entrust.
LoseDevice(Invr) @ #invrLose &
EntrustSent(fid, anyone, secretHolder) @ #entrust &
LoseDevice(secretHolder) @ #fusionSecretLose &
#invrLose < #added &
#fusionSecretLose < #added
)
)"
Note the subtle difference between EntrustSent (in case 3) and StateChange_LearnFusionSecret (in case 2): One fact is emitted when the encrypted entrust message is sent, and one when it is received.
Tombstoning Authorization
To ensure that only members of a fusion identity can tombstone the identity, we say that a fusion identity can only be tombstoned if the recipient knows the sender of the tombstone message is in the fusion identity before the tombstone message is receeived, with the exception that the sender could have also lost their device.
lemma tombstone_authorization:
"All fid rcvr sender #received #joined.
(
(
StateChange_AddToFusionID(rcvr, fid, sender) @ #joined & // rcvr knows sender is in FID
StateChange_FID_Tombstoned(rcvr, fid, sender) @ #received & // msg received
not (sender = rcvr)
) ==> (
(
Ex #tombstoned.
StateChange_FID_Tombstoned(sender, fid, sender) @ #tombstoned & // sender tombstones
#joined < #received &
#tombstoned < #received
) | (
Ex #lose.
LoseDevice(sender) @ #lose &
#lose < #received
)
)
)"
Key Is Entrusted Only to Devices that Have Consented to the Fusion Identity
We specify that for an Entruster to entrust another device that the entrusting device has not been lost and the entrusted device has previously consented to the invitation to the fusion identity.
lemma key_is_entrusted_only_to_consenting_devices:
// for all devices, only devices that have consented to the fusion ID are entrusted with the key
"All Entruster Entrustee fid #txEntrust. (
(
StateChange_MarkingEntrusted(Entruster, fid, Entrustee) @ #txEntrust
& ( not Ex #loseDevice. (
(LoseDevice(Entruster) @ #loseDevice & #loseDevice < #txEntrust)
//| (LoseDevice(Entrustee) @ #loseDevice & #txEntrust < #loseDevice)
)
)
) ==> (
Ex #rxConsent. (
StateChange_ConsentedToFusionID(Entruster, fid, Entrustee) @ #rxConsent
& #rxConsent < #txEntrust
)
)
)"
Limitations
Because the redirect and attestation system involves out of band communications and voting methods that cannot be modelled in Tamarin, we were not able to model or provide security proofs on this portion of the protocol.
Observations
The specification was not precise with regards to message format and state transitions. This means that our efforts at modelling the protocol represent our interpretation of the specification and that implementors might have a different interpretation, in which their implementation might diverge from our model (see Issue B).
Additionally, in some instances the modelled protocol slightly deviates from the specified protocol. The main reason for that is that in Tamarin, modelling the referencing of messages by hash is not trivial, which means we didn’t include tangles or other kinds of references in the model. However, if the real protocol messages contain at least all the information as the modelled protocol messages, the security of the real protocol is implied.
Implementation Considerations
Observations
When implementing the protocol, state transitions have to be done according to the protocol spec, or rather the modelled protocol, since the spec is not very precise. Because of the imprecision, we had to interpret a bit during the formal analysis and accordingly the results of the formal analysis do not necessarily translate to other implementations. Since the Scuttlebutt community is diverse, implementations should follow our interpretation to guarantee the security provided in our proofs.
Future Work
Our proposed protocol extension in Suggestion A has not been modelled. Future work could model the extension and guide the design of the protocol extension.
While the Tamarin code was written with best practices in mind, we believe there are still areas that could benefit from refactoring and further scrutiny.
Issues
Issue A: Specification Is Not Precise Enough
We found the specification to be vague with respect to the expected state of the devices when receiving and sending messages, in particular, under which conditions are entities allowed to receive and send messages.
For example, for invite messages the protocol specification states “Only a feed that was either the one that created the fusion identity or has accepted an invite is allowed to create an invite.” While this might guide the implementors of an SSB client, it does not define rules which would restrict the behavior of an attacker. A clearer specification would outline which rules must be satisfied in order to process a received message. These rules would require reference to variables (in pseudocode) that refer to earlier steps in the protocol.
Issue B: No Forward Secrecy
Most if not all modern secure communication protocols provide forward secrecy. This security property describes that encrypted messages sent before a device was corrupted remain secret. In the Scuttlebutt ecosystem, very few components satisfy this notion. We recommend that a forward-secret version of encrypted messages be added.
Suggestions
Suggestion A: Explore Protocol Extension for Authentication for Redirects
After a Fusion Identity has been tombstoned, the protocol specifies a system for publishing redirects. Because at this state of the protocol it is unknown which of the tombstoned fusion identity’s devices can be trusted, a voting system is outlined in the protocol, where users can attest to a redirect. This requires out of band communication for users to verify which redirect is the correct one. While this works for many members of the SSB community that have other means of communicating, for users that are not connected outside the network, this system has drawbacks.
We propose a protocol extension where redirects are authenticated by the individual that generated the original fusion identity. The security of a scuttlebutt identity is based on what a user has, i.e. their private key. For a fusion identity, the secret key of the fusion identity is shared by all devices. In the event that a device is lost or compromised, the security model based on what a user has becomes broken. Because of this, implementing a model based on what the user knows could supplement the redirect process because the user of a compromised device would not know the secret.
The proposed scheme would work as follows: when a user generates a fusion identity, they create a memory based secret (i.e. password), that is passed to a key derivation function and then hashed with a secure hashing algorithm. This hash is then published along with the fusion identity. When the user tombstones their fusion identity and publishes a redirect, the redirect is guaranteed to be authentic because a proof of knowledge of the hash’s preimage (produced by the key derivation function, and not the password itself) is published with the redirect. Because other users can confirm that the redirect is valid by reproducing the hash from the fusion identity initialization, they will know that the redirect was published by the user that created the original fusion identity. This system would allow redirects to be trusted without using any out of band communications or attestation systems.
Suggestion B: There are no Recommendations for how to Protect Private Keys
The protocol operates on the assumption that private keys are maintained private. The security of private keys is then a responsibility for the implementation of the protocol in various clients. Because private keys are stored as regular files on the user’s filesystem without special permissions, it only takes a drive-by browser exploit for a private key to become compromised. We recommend that the protocol outline recommendations for those implementing clients where the key should be stored according to security best practices. For instance, using a secure storage mechanism such as a key chain, or encrypting the private key when at rest.
Appendix
Appendix A: Source Code of Sequence Diagram
The source code can be processed using blockdiag or kroki.io in SeqDiag mode.
seqdiag {
user --> laptop [label = "UI: create fusion id"] {
laptop ->> laptop [note = "generate:\nfuSec = rand(); fid = pk(fuSec)\npublish:\n('fusion-id/init', fid, pop)"]
}
user <-- laptop [label = "created fusion id 'fid'"]
user --> laptop [label = "UI: invite phone to fid"]{
laptop ->> phone [note = "publish:\n('fusion-id/invite', fid, phone)"]{
phone --> user [label="UI: received invite to fid from laptop"]
phone <-- user [label="UI: accept"]
}
laptop <<- phone [note = "publish:\n('fusion-id/accept', fid)"]
}
user <-- laptop [label = "UI: phone has accepted. entrust?"];
user --> laptop [label = "UI: entrust key"] {
laptop ->> phone [note = "publish DM@phone:\n ('fusion-id/entrust', fid, fuSec)"] {
phone --> user [label = "UI: received entrust from laptop"]
phone <-- user [label = "UI: publish proof and complete"]
}
laptop <<- phone [note = "publish:\n('fusion/proof', fid, sign('proof', fid, phone))"]
}
user <-- laptop [label ="UI: phone joined fusion id!"]
=== user loses phone ===
user --> laptop [label = "UI: tombstone fusion id"] {
laptop ->> laptop[note = "publish:\n('/fusion/tombstone', fid)"];
}
user <-- laptop;
user --> laptop [label = "UI: create new fusion id"] {
laptop ->> laptop [note = "generate:\nfuSec = rand(); fid = pk(fuSec)\npublish:\n('fusion-id/init', fid, pop)"]
}
user <-- laptop;
user --> laptop [label = "UI: redirect old to new fusion id"] {
laptop ->> laptop [note = "publish:\n('/fusion/redirect', old_fid, new_fid)"]
};
user <-- laptop;
user --> laptop [label = "UI: sync with network"] {
laptop -> alice [label = "sync"]
laptop <- alice [note = "alice accepts in the UI.\npublish:\n('/fusion/attest', old_fid, new_fid, 'accept')"]
laptop -> bob [label = "sync"];
laptop <- bob [note = "bob rejects in the UI.\npublish:\n('/fusion/attest', old_fid, new_fid, 'reject')"]
}
user <-- laptop [label = "UI: alice has accepted;\nbob has rejected."]
}
Appendix B: Tamarin Source Code
theory ScuttlebuttFusionIdentities
begin
builtins: hashing, signing, asymmetric-encryption
// register new devices in the model
// there is an AA at the front so it's first when sorted by byte value. this is important so it picks this one first.
rule AARegister_Device:
let
devVK = pk(~devSK)
in
[ Fr(~devSK) ]
--[ NewDevice(devVK, ~devSK) ]->
[
!Device(devVK),
Out(devVK)
]
rule Lose_Device:
let
devVK = pk(devSK)
in
[ !Device(devVK) ]
--[ LoseDevice(devVK) ]->
[ !DeviceLost(devVK)
, Out(devSK) ]
rule Initialize_FusionID:
let
fid = pk(~fusionSecret)
devVK = pk(devSK)
msg = <'init', devVK, fid>
signedInitMsg = <msg, sign(msg, devSK)>
in
[ !Device(devVK)
, Fr(~fusionSecret) ]
--[
InitFusionID(fid, devVK, ~fusionSecret),
StateChange_AddToFusionID(devVK, fid, devVK),
StateChange_LearnAboutFusionID(devVK, fid),
StateChange_LearnFusionSecret(devVK, fid, ~fusionSecret)
]->
[ !FusionID(fid)
, !State_IsInFusionID(devVK, fid, devVK)
, !State_KnowsFusionID(devVK, fid)
, !State_KnowsFusionSecret(devVK, fid, ~fusionSecret)
, Out(signedInitMsg)
]
rule ReceiveInitMsg:
let
initorVK = pk(initorSK)
msg = <'init', initorVK, fid>
signedInitMsg = <msg, sign(msg, initorSK)>
in
[ !Device(initorVK)
, !Device(rcptVK)
, In(signedInitMsg) ]
--[
StateChange_LearnAboutFusionID(rcptVK, fid),
StateChange_AddToFusionID(rcptVK, fid, initorVK)
]->
[
!State_KnowsFusionID(rcptVK, fid),
!State_IsInFusionID(rcptVK, fid, initorVK)
]
rule SendInvite:
let
InvrVK = pk(InvrSK)
//
invTxt = <'invite', fid, InvrVK, InveeVK>
sig = sign(invTxt, InvrSK)
invitation = <invTxt, sig>
in
[
In(InveeVK),
!State_KnowsFusionID(InvrVK, fid),
!State_IsInFusionID(InvrVK, fid, InvrVK), // might not matter. what really matters is whether recipient knows Invr is in Fid
!Device(InvrVK),
In(InveeVK)
]
--[
InviteSent(fid, InvrVK, InveeVK),
StateChange_IsInvited(InvrVK, fid, InveeVK)
]->
[
Out(invitation),
State_IsInvited(InvrVK, fid, InveeVK)
]
rule ReceiveInvite:
let
InvrVK = pk(InvrSK)
//
invTxt = <'invite', fid, InvrVK, InveeVK>
sig = sign(invTxt, InvrSK)
invitation = <invTxt, sig>
in
[
!FusionID(fid),
!Device(InvrVK),
!Device(rcptVK),
!State_IsInFusionID(rcptVK, fid, InvrVK),
In(invitation)
]
--[
StateChange_IsInvited(rcptVK, fid, InveeVK),
InvitedBy(InvrVK),
NotEqual(InvrVK, InveeVK)
]->
[
State_IsInvitedBy(rcptVK, fid, InveeVK, InvrVK)
]
rule AcceptInvite:
let
InvrVK = pk(InvrSK)
InveeVK = pk(InveeSK)
//
acceptTxt = <'accept', fid, InveeVK>
acceptSig = sign(acceptTxt, InveeSK)
acceptMsg = <acceptTxt, acceptSig>
in
[
!FusionID(fid),
!Device(InvrVK),
!Device(InveeVK),
State_IsInvitedBy(InveeVK, fid, InveeVK, InvrVK),
!State_IsInFusionID(InveeVK, fid, InvrVK)
]
--[
StateChange_IsInvited(InveeVK, fid, InveeVK),
StateChange_ConsentedToFusionID(InveeVK, fid, InveeVK),
InvitedBy(InvrVK)
]->
[
State_ConsentsToFusionIDBy(InveeVK, fid, InveeVK, InvrVK),
Out(acceptMsg)
]
rule ReceiveAccept:
let
InveeVK = pk(InveeSK)
//
acceptTxt = <'accept', fid, InveeVK>
acceptSig = sign(acceptTxt, InveeSK)
acceptMsg = <acceptTxt, acceptSig>
in
[
In(acceptMsg),
!Device(InveeVK),
!Device(InvrVK),
!Device(rcptVK),
State_IsInvitedBy(rcptVK, fid, InveeVK, InvrVK)
]
--[
StateChange_ConsentedToFusionID(rcptVK, fid, InveeVK)
]->
[
State_ConsentsToFusionIDBy(rcptVK, fid, InveeVK, InvrVK) // recipient stores Invee's Consent to FID from the Invite By Invr
]
rule SendEntrust:
/*{
type: 'fusion/entrust',
secretKey: KEY, // make this consistent
fusionRoot: %init,
recps: [@fusionA, @feedDesktop]
}*/
let
InvrVK = pk(InvrSK)
InveeVK = pk(InveeSK)
fid = pk(fusionSecret)
//
entrustPlain = <'entrust', fid, InvrVK, fusionSecret>
entrustEncrypted = aenc(entrustPlain, InveeVK)
entrustSig = sign(entrustEncrypted, InvrSK)
outMsg = <entrustEncrypted, entrustSig>
in
[ !Device(InvrVK)
, !FusionID(fid)
, State_ConsentsToFusionIDBy(InvrVK, fid, InveeVK, InvrVK)
, !State_IsInFusionID(InvrVK, fid, InvrVK)
, !State_KnowsFusionSecret(InvrVK, fid, fusionSecret)
]
--[
EntrustSent(fid, InvrVK, InveeVK),
StateChange_MarkingEntrusted(InvrVK, fid, InveeVK)
]->
[
Out(outMsg),
State_IsEntrusted(InvrVK, fid, InveeVK)
]
rule SendProofOfKey:
/*{
type: fusion/proof-of-key,
consentId: %consent,
proof: sign(%consent + 'fusion/proof-of-key')
tangles: {
fusion: { root, previous }
}
}*/
let
InvrVK = pk(InvrSK)
InveeVK = pk(InveeSK)
fid = pk(fusionSecret)
//
entrustPlain = <'entrust', fid, InvrVK, fusionSecret>
entrustEncrypted = aenc(entrustPlain, InveeVK)
entrustSig = sign(entrustEncrypted, InvrSK)
inMsg = <entrustEncrypted, entrustSig>
//
pok_inner = <'pok_inner', InveeVK, fid>
pok_inner_sig = sign(pok_inner, fusionSecret)
pok_outer = <'pok', pok_inner_sig>
pok_outer_sig = sign(pok_outer, InveeSK)
pok = <pok_outer, pok_outer_sig>
in
[
!FusionID(fid),
In(inMsg),
!Device(InvrVK),
!Device(InveeVK)
] --[
AddedByInvitation(InvrVK),
StateChange_ProvidedProofOfKey(InveeVK, fid),
StateChange_AddToFusionID(InveeVK, fid, InveeVK),
StateChange_LearnFusionSecret(InveeVK, fid, fusionSecret)
]->
[
Out(pok)
, !State_IsInFusionID(InveeVK, fid, InveeVK)
, !State_KnowsFusionSecret(InveeVK, fid, fusionSecret)
]
rule ReceiveProofOfKey:
let
InveeVK = pk(InveeSK)
fid = pk(fusionSecret)
//
pok_inner = <'pok_inner', InveeVK, fid>
pok_inner_sig = sign(pok_inner, fusionSecret)
pok_outer = <'pok', pok_inner_sig>
pok_outer_sig = sign(pok_outer, InveeSK)
pok = <pok_outer, pok_outer_sig>
in
[ In(pok)
, !Device(RcvrVK)
, !Device(InveeVK)
, !Device(InvrVK)
]
--[ StateChange_AddToFusionID(RcvrVK, fid, InveeVK) ]->
[ !State_IsInFusionID(RcvrVK, fid, InveeVK)
]
/*{
type: 'fusion/tombstone',
reason: 'Lost @feedPhone, state of key is unknown',
tangles: {
fusion: {
root: %init,
previous: [%consent]
}
}
}
RULES:
you cannot undo a tombstone
once a tombstone has been published, the only messages which are allowed
to extend the tangle are other tombstone messages
you MUST NOT DM a tombstoned identity
NOTE:
tangles can have divergent state (many tips to the graph).
We consider a tangle tombstoned if any of the tips are a tombstone message
*/
rule SendTombstone:
let
fid = pk(fusionSecret)
TomberVK = pk(TomberSK)
tombstone_message = <'tombstoned', fid, TomberVK>
sig = sign(tombstone_message, TomberSK)
msg = <tombstone_message, sig>
in
[
!Device(TomberVK),
!State_IsInFusionID(TomberVK, fid, TomberVK)
]
--[
StateChange_FID_Tombstoned(TomberVK, fid, TomberVK)
]->
[
Out(msg),
!State_IsTombstoned(TomberVK, fid, TomberVK)
]
rule ReceiveTombstone:
let
fid = pk(fusionSecret)
TomberVK = pk(TomberSK)
RecvVK = pk(RecvSK)
tombstone_message = <'tombstoned', fid, TomberVK>
sig = sign(tombstone_message, TomberSK)
signed_msg = <tombstone_message, sig>
in
[
In(signed_msg),
!Device(TomberVK),
!Device(RecvVK),
!State_IsInFusionID(RecvVK, fid, TomberVK)
]
--[
StateChange_FID_Tombstoned(RecvVK, fid, TomberVK)
]->
[
!State_IsTombstoned(RecvVK, fid, TomberVK)
]
rule SendRedirect:
let
oldFID = pk(fusionSecret)
newFID = pk(~newFusionSecret)
SenderVK = pk(SenderSK)
//
redirectBody = <'redirect', SenderVK, oldFID, newFID>
redirectSig = sign(redirectBody, SenderSK)
redirect = <redirectBody, redirectSig>
in
[
!Device(SenderVK),
!State_IsInFusionID(SenderVK, oldFID, SenderVK),
!State_IsInFusionID(SenderVK, newFID, SenderVK),
!State_IsTombstoned(SenderVK, oldFID, SenderVK) // this might not be actually how the protocol works, since the redirect is an independent tangle
]
--[
!StateChange_SendRedirect(SenderVK, oldFID, newFID)
]->
[
Out(redirect),
!State_RedirectSent(SenderVK, oldFID, newFID)
]
rule ReceiveRedirect:
let
SenderVK = pk(SenderSK)
//
redirectBody = <'redirect', SenderVK, oldFID, newFID>
redirectSig = sign(redirectBody, SenderSK)
redirect = <redirectBody, redirectSig>
in
[ !Device(RcvrVK)
, !Device(SenderVK)
, !State_IsInFusionID(RcvrVK, oldFID, SenderVK)
, !State_IsInFusionID(RcvrVK, newFID, SenderVK)
, In(redirect)
]
--[
StateChange_RedirectReceived(RcvrVK, oldFID, newFID, SenderVK)
]->
[ State_RedirectHintReceived(RcvrVK, oldFID, newFID, SenderVK)
]
// attestationPosition is either "accept" or "reject"
// tombstoning attestations is not modelled because we are not sure it's a good idea
rule AttestRedirect:
let
AttestorVK = pk(AttestorSK)
//
attestationBody = <'attest', AttestorVK, oldFID, newFID, attestationPosition>
attestationSig = sign(attestationBody, AttestorSK)
attestation = <attestationBody, attestationSig>
in
[ !Device(AttestorVK)
, !State_IsInFusionID(AttestorVK, oldFID, SenderVK)
, !State_IsInFusionID(AttestorVK, newFID, SenderVK)
, State_RedirectHintReceived(AttestorVK, oldFID, newFID, SenderVK)
, In(attestationPosition)
]
--[
StateChange_RedirectAttested(AttestorVK, oldFID, newFID, SenderVK, attestationPosition)
]->
[ Out(attestation)
, State_RedirectAttested(AttestorVK, oldFID, newFID, AttestorVK, attestationPosition)
]
/// RESTRICTIONS
/// not needed if we check signatures pattern-matching style:
// restriction only_valid_signatures:
// For all traces that contain trace facts Signed(sig, txt, pk), only consider those traces, where verify(sig, txt, pk) returns true
// for all sent invites, there does not exist an addtofusionid fact from before the invite was sent
restriction dont_invite_members:
"All Invr Invee fid #tInvite.
InviteSent(fid, Invr, Invee) @ #tInvite ==> (
not Ex #tAddTo. (
StateChange_AddToFusionID(Invr, fid, Invee) @ #tAddTo &
#tAddTo < #tInvite
)
)"
restriction enforce_not_equal:
"All left right #time. NotEqual(left, right) @ #time ==> not (left = right)"
restriction enforce_attestation_position:
"All Attestor oldFid newFid SenderVK attestationPosition #i.
StateChange_RedirectAttested(Attestor, oldFid, newFid, SenderVK, attestationPosition) @ #i ==> (
attestationPosition = 'accept' | attestationPosition = 'reject')"
restriction receive_init_only_once:
"All fid devA devB #i #j. (
StateChange_AddToFusionID(devA, fid, devB) @ #i &
StateChange_AddToFusionID(devA, fid, devB) @ #j
) ==> #i = #j"
/// FORALL-TRACE LEMMAS (security)
// lemma to prove the conditions underwhich fusionSecret is actually secret
lemma fusion_secret_secrecy:
// there do not exist
"not (Ex initor fid fusionSecret #init #learn.
// a fusion id `fid` and matching secret `fusionSecret`
InitFusionID(fid, initor, fusionSecret) @ #init &
// and the adversary knows the secret
K(fusionSecret) @ #learn &
// and neither the initiator
not (Ex #lose. LoseDevice(initor) @ #lose) &
// nor a party the key was legally entrusted to lost their keys
not (Ex anyEntruster anyEntrustee #entrust #lose.
EntrustSent(fid, anyEntruster, anyEntrustee) @ #entrust &
LoseDevice(anyEntrustee) @ #lose
)
)"
// Invee has been added to the fusion ==> Ex Inver. Inver is in the fid AND ( Inver invited invee OR Inver was hacked)
lemma membership_soundness:
"All Invee Invr fid #added.
(
StateChange_AddToFusionID(Invee, fid, Invee) @ #added &
AddedByInvitation(Invr) @ #added
) ==> (
// case 1: proper invitation flow
(Ex #invrAdded #invite.
StateChange_AddToFusionID(Invr, fid, Invr) @ #invrAdded &
InviteSent(fid, Invr, Invee) @ #invite &
#invite < #added
) |
// case 2: the attacker takes over a member
(Ex fusionSecret #lose #learn.
LoseDevice(Invr) @ #lose &
StateChange_LearnFusionSecret(Invr, fid, fusionSecret) @ #learn &
#learn < #added
) |
// case 3: the attacker stole a device that was entrusted the secret and steals some other device to send the entrust from
(Ex anyone secretHolder #invrLose #fusionSecretLose #entrust.
LoseDevice(Invr) @ #invrLose &
EntrustSent(fid, anyone, secretHolder) @ #entrust &
LoseDevice(secretHolder) @ #fusionSecretLose &
#invrLose < #added &
#fusionSecretLose < #added
)
)"
// for all tombstone messages received, the signer of the message was in the fusionID or the device was lost
lemma tombstone_authorization:
"All fid rcvr sender #received #joined.
(
(
StateChange_AddToFusionID(rcvr, fid, sender) @ #joined & // rcvr knows sender is in FID
StateChange_FID_Tombstoned(rcvr, fid, sender) @ #received & // msg received
not (sender = rcvr)
) ==> (
(Ex #tombstoned.
StateChange_FID_Tombstoned(sender, fid, sender) @ #tombstoned & // sender tombstones
#joined < #received &
#tombstoned < #received
) |
(Ex #lose.
LoseDevice(sender) @ #lose &
#lose < #received
)
)
)"
lemma only_accept_when_invited:
"All Inver Invee fid #accept. (
StateChange_ConsentedToFusionID(Invee, fid, Invee) @ #accept &
InvitedBy(Inver) @ #accept
) ==> (
(Ex #send.
InviteSent(fid, Inver, Invee) @ #send &
#send < #accept
) | (Ex #lost.
LoseDevice(Inver) @ #lost &
#lost < #accept
)
)"
lemma key_is_entrusted_only_to_consenting_devices:
// for all devices, only devices that have consented to the fusion ID are entrusted with the key
"All Entruster Entrustee fid #txEntrust. (
(
StateChange_MarkingEntrusted(Entruster, fid, Entrustee) @ #txEntrust &
not (Ex #loseDevice.
LoseDevice(Entruster) @ #loseDevice &
#loseDevice < #txEntrust
)
) ==> (Ex #rxConsent.
StateChange_ConsentedToFusionID(Entruster, fid, Entrustee) @ #rxConsent &
#rxConsent < #txEntrust
)
)"
/// EXISTS-TRACE LEMMAS (model sanity)
lemma device_can_see_other_memberships: exists-trace
"Ex devA devB fid #addA.
StateChange_AddToFusionID(devA, fid, devB) @ #addA &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma device_can_invite: exists-trace
"Ex devA devB fid #addA #addB.
StateChange_AddToFusionID(devA, fid, devA) @ #addA &
StateChange_IsInvited(devA, fid, devB) @ #addB &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma device_can_be_invited: exists-trace
"Ex devA devB fid #addA #addB.
StateChange_AddToFusionID(devA, fid, devA) @ #addA &
StateChange_IsInvited(devB, fid, devB) @ #addB &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma device_can_send_accept: exists-trace
"Ex devA devB fid #addA #addB.
StateChange_AddToFusionID(devA, fid, devA) @ #addA &
StateChange_ConsentedToFusionID(devB, fid, devB) @ #addB &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma device_can_receive_accept: exists-trace
"Ex devA devB fid #addA #addB.
StateChange_AddToFusionID(devA, fid, devA) @ #addA &
StateChange_ConsentedToFusionID(devA, fid, devB) @ #addB &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma device_can_send_entrust: exists-trace
"Ex devA devB fid #addA #entrust.
StateChange_AddToFusionID(devA, fid, devA) @ #addA &
EntrustSent(fid, devA, devB) @ #entrust &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma fusion_id_has_two_devices: exists-trace
"Ex devA devB fid #addA #addB.
StateChange_AddToFusionID(devA, fid, devA) @ #addA &
StateChange_AddToFusionID(devA, fid, devB) @ #addB &
not devA=devB &
not (Ex #lose. LoseDevice(devA) @ #lose) &
not (Ex #lose. LoseDevice(devB) @ #lose)"
lemma fusion_id_can_be_tombstoned: exists-trace
"Ex dev fid #tombstoned.
StateChange_FID_Tombstoned(dev, fid, dev) @ #tombstoned
"
lemma tombstoning_by_someone_else_than_initor_works: exists-trace
"Ex devInit devTomb fid secret #tombstoned #init.
StateChange_AddToFusionID(devInit, fid, devInit) @ #init &
InitFusionID(fid, devInit, secret) @ #init &
StateChange_FID_Tombstoned(devTomb, fid, devTomb) @ #tombstoned &
not (
devInit = devTomb |
(Ex anyDev #lose. LoseDevice(anyDev) @ #lose)
) &
#init < #tombstoned
"
lemma device_can_observe_tombstoning_by_someone_else_than_initor: exists-trace
"Ex devInit devTomb devObs fid secret #tombstoned #init.
StateChange_AddToFusionID(devInit, fid, devInit) @ #init &
InitFusionID(fid, devInit, secret) @ #init &
StateChange_FID_Tombstoned(devObs, fid, devTomb) @ #tombstoned &
not (
devInit = devTomb | devTomb = devObs |
(Ex anyDev #lose. LoseDevice(anyDev) @ #lose)
) &
#init < #tombstoned
"
lemma device_can_observe_accept_attestation: exists-trace
"Ex AttestorVK SenderVK oldFID newFID #i.
StateChange_RedirectAttested(AttestorVK, oldFID, newFID, SenderVK, 'accept') @ #i &
not SenderVK = AttestorVK
"
end
Audit Report: Secure Scuttlebutt Partial Replication and Fusion Identity
Authors: Justin Regele (Arxum Path Security GmbH), Jan Winkelmann
Introduction
This reports documents the findings from the audit of the Secure Scuttlebutt Partial Replication and Fusion Identity specifications. While we did not find any immediate security concerns, we do provide suggestions below on areas that could be improved. Our research also included a formal analysis, i.e. a mathematical modeling, of the Fusion Identity protocol, where we found that the security properties of the protocol hold under the assumptions of our model. We do note that our model is our interpretation of the protocol, and therefore the security of a particular implementation of the protocol will be conditional to its adherence to our model.
The report begins with a summary, describing the protocols, our methodology, and a high level overview of our suggestions. This is followed by a short section on partial replication in which we discuss the work performed during this phase of the audit. The remainder of the report documents in depth our formal analysis of the Fusion Identity protocol. We discuss at a high level how we modelled the protocol using the Tamarin Prover, and then document our Rules and Lemmas individually so that the reader can understand our intentions behind the code associated with this report.
This section is then followed by the Issues and Suggestions, and we conclude with our thoughts on further work.
Summary / Gist
We report on our analysis of two new subcomponents in the Secure Scuttlebutt ecosystem: The Fusion ID mechanism and the partial replication protocol. The specification documents in scope are:
Meta Feeds are a core piece of the partial replication protocol designed by the SSB NGI Pointer team. It describes a standard way to build hierarchical feeds, where there is a single root feed and multiple subfeeds. These subfeeds can be used for different purposes, including maintaining indexes of messages. For example, One feed could be the main feed where messages are posted as they are in the current version of Scuttlebutt, and additionally there could be a feed that posts references to all messages that are of type “post”. This would be done with the goal of quickly finding all post messages by that user.
The Fusion ID protocol is a way to join multiple feeds into a single logical identity. The main motivation here is that in Scuttlebutt, users have multiple devices, but each device must have its own Scuttlebutt feed due to synchronization issues. Fusion IDs are an attempt to mitigate the impact on the user experience this technical limitation has.
The partial replication protocol was assessed through the means of a manual review of the specification, as well as clarifying conversations with the authors of the specification.
The Fusion ID protocol was reviewed more rigorously, using formal methods, i.e. a sound mathematical model. Specifically, we use the Tamarin prover to model the protocol and the security properties we expect to hold.
Additionally, an early review of parts of the Rooms 2 Specification was performed in pull requests #17 and #18. Some changes were recommended and quickly applied to the specification. In particular, signed strings should include a reference to the rooms protocol in order to avoid the possiblity of interactions with other protocols. More importantly, however, is that the authenticating signatures should contain the nonces of both parties, in order to guarantee liveness of both parties. Since the nature of this work was an early design consultation, we do not mark the recommended changes as issues in this report.
We did not find immediate security issues in the security components in scope. However, we noticed that in several parts, the specification was not very precise and left room for interpretation. In the context of our work we were able to get clarifications of what the intended protocol mechanisms were, and used these in our modeling. Other parties will however implement their own, possibly different, interpretation of the specification, which may lead to incompatibility or invalidation of our security analysis (see Issue A).
Additionally, we suggest further development of the protocol by adding a protocol extension for improving the trust placed in redirects (see Suggestion A). Furthermore, we advocate making recommendations for secure storage of the keys used in the protocol, and clearly specifying which values should be considered secret (see Suggestion B).
The formal analysis however showed that, based on the assumptions made in the model, the protocol is secure according to the security properties we defined. The two central security properties are fusion secret secrecy and membership soundness, which, besides some additional ones, are described in the Lemmas section.
With regard to the general approach to security, however, we do have to note two shortcomings. Firstly, only the transport encryption protocol provides forward secrecy (see Issue B). This is a security property that should be provided by a modern communication protocol. Secondly, the storage of private keys lacks a description of security best practices (see Suggestion B).
Partial Replication
The partial replication specification was reviewed manually and questions were discussed with the authors. The feed format for Meta feeds was discussed and the Bendy Butt format was agreed upon as the best suited for the protocol.
When discussing the derivation of signing keys of the different feeds, it was recommended that a salt should be used to derive the signing keys, e.g. using HMAC. This would allow a deterministic derivation of all signing keys from a single secret seed. It was recommended that 32 bytes was sufficient input for the seed. Additionally, 32 bytes was agreed upon for the size of the nonce, and that random data could be used for the nonce instead of a timestamp, since collisions on random 256-bit values are negligibly rare.
In the design of subprotocols that make use of signing, it is important to keep the domains of SSB messages signing and the different subprotocols separated. We found that the team has done a good job doing this.
The trust model for auditing claims was discussed. One potential concern for the system was regarding incentives for members of the network to perform audits of claims. In situations where all of the users are using thing clients, auditing claims would not be feasible, as auditing requires resources not available on mobile devices. This could result in centralization as specific nodes would handle all the auditing, and therefore trust would be centralized to these nodes. This is more of a concern regarding decentralization than the security of the protocol. However, if decentralization itself is considered a security property for the network, then the centralizating of auditing nodes could pose a security concern. If partial replication is dependent on a small number of nodes, the trustworthiness of these nodes (i.e. have they been compromised) would affect the trustworthiness of the partial replication protocol. Despite the emphasis on decentralization, the existence of pubs demonstrates that some centralization is useful for the ecosystem’s usability. It was concluded that as long as auditing nodes were not reduced to a single point of failure, nodes coming to consensus on auditing claims would work securely much as they do in a setting involving a blockchain.
Fusion Identity Protocol
In this section we take a closer look at the Fusion ID protocol. First we describe the features and the protocol flow. In subsection Audit we present the results of our manual review. In Formal Analysis we first provide an introduction to the tool we used, then explain how we modelled the protocol and security properties, go into limitations of the system and finally present the results.
Description
The protocol flow is described in the following sequence diagram:
The source code for this diagram can be found in Appendix A.
Formal Analysis
There are several methodologies for rigorously analyzing the security of a protocol. When it comes to cryptographic protocols, the computational model is usually considered the strongest. However, performing analyses in this model is very complex, and focuses more on the security of the cryptographic components, rather than logic errors.
Formal methods are an approach that have its origins in type theory and have been used for verifying program correctness for a long time. Since then, theories for many cryptographic algorithms have been introduced, allowing to model cryptographic protocols as well.
In this work we use the Tamarin prover. It provides theories for many common cryptographic primitives and reasons about network flow and attacker knowledge. The source code of the model we developed can be found in Appendix B.
In our analysis, we showed that all security properties we formulated hold for the modelled protocol.
The rest of this section is structured as follows: First we give a brief introduction to the way protocols and security properties are modelled in Tamarin. Then we provide an overview over the way the Fusion ID protocol is modelled, and then into how the security properties we aim for are modelled. We conclude with a brief section that discuss the limitations of this approach.
Modelling in Tamarin
The fundamental concept is as follows: The modeller describes rules that modify the current state of the “modelled world”. That world is modelled as a collection of so called facts, which are atomic state objects such as
UserIsInvited(uid, fid)to denote that the user with iduidis invited to fusion idfid.A rule can change that world by consuming old and producing new facts. For example, there could be a rule where the
UserIsInvitedfact is consumed and replaced with aUserHasAcceptedfact.Tamarin provides some special facts that help with modelling cryptographic protocols. Firstly, there is the
Fr(for fresh) fact, which is used to create new random values. Secondly, there are theInandOutfacts, which are used to model both network interaction and attacker knowledge; a rule can consume a factIn(msg), which represents receiving a message, and produce anOut(msg)fact, which represents sending one. The network model of Tamarin is simple: It assumes that all that is sent to the network is received by the adversary, which is then able to provide it as input to any rule consuming anInfact (assuming the rule is fulfilled).Rules usually consume and produce more than one fact, and the data that is contained in these facts is usually related. For example, a rule can consume a signed message, and the key used for signing must match a that of a registered user. This means, that rules are used to model the correct flow of the protocol, but as soon as the attacker learns a secret, they can also use it for signing, encrypting or decrypting, and then use values they learned from this as well.
Each sequence of application of rules will lead to a different collection of facts. In Tamarin, security properties are defined by declaring that in all valid applications of rules, a certain invariant holds. In order to formulate these statements, we need another class of facts. To not confuse our terminology too much, lets call the facts from earlies state facts (because they describe the state of the model). This new class of facts is called action facts. Rules can also specify to produce those, but these can not be consumed later on. Instead, they are written to a trace, which describes the sequence of all rules that have been applied.
The security properties are then formulated as lemmas, which are logic statements over predicates, quantified over all possible traces - either formulated as “for all” or “there does not exist”. There is another feature that uses this kind of statement: restrictions. These can be used to limit the traces that are being analyzed. In our model one example we use these for is to prevent parties from inviting themselves.
As a side note: there also are lemmas of the form “there exists a trace”. This is used for sanity-checking the model, i.e. to ensure that there even exists a way for the protocol to terminate as intended.
Rules
Here we document the rules in our Model. We begin with the first rules in more detail, explaining the syntax of each rule, along with its intention. Later we move onto only explaining the rule’s intention, as the reader comes to understand Tamarin’s syntax.
Register Device
The
AARegisterDeviceRule is named because Tamarin uses alphabetic sorting to choose cases to search. We found that by naming this rule with a prepended AA, this solved problems of Tamarin becoming lost and getting caught in endless loops during automated proving. The defined rule is as follows:The rule defines a device, which uses pattern matching to pair the device’s signing key
devSKwith the device’s verification keydevVK.Fr(~devSK)instructs Tamarin to generate a fresh signing key for this device as an input fact. The action factNewDevice(devVK, ~devSK)registers this new Device.!Device(devVK)in the output facts means the device is now available in the system and is persistent and will not disappear when consumed by other rules (indicated by the!).Out(devVK)means that the device’s verification key is now publicly available.Lose Device
The Lose_Device rule takes in a Device, and outputs a DeviceLost fact for that device VK, along with the SK for the device. The Action fact for this rule is simply
LoseDevice.Initialize FusionID
This rule models the initialization of a Fusion Identity. Its inputs are:
In the action traces, the rule models the following states changes:
The rules output states appear similar to the state changes in the action traces.
State_IsInFusionIDandState_KnowsFusionIDappear similar toStateChange_AddToFusionIDandStateChange_LearnAboutFusionID. However, the distinction is important for Tamarin as they are different types of facts. Within the trace are action facts, which indicate a change, whereas the facts in the output indicate the result.Receive Init Message
ReceiveInitMsgtakes aninitor(initiator) and arcpt(recipient), and models another device on the network observing that a the fusion id has been intialized.State_Change_AddToFusionID(rcptVK, fid, initorVK)means thatrcptVKnow knows that theinitorVKis in fusion idfid.Send Invitation
SendInvite models the sending of an invite to join the fusion identity. The input requirements are that the invitor knows the fusion identity and is a part of it. The invitee is an arbitrary input. The state changes are that the invite has been sent and that the invitor knows that the invitee has been invited.
Receive Invitation
Models the reception of an invite. The rule requires a fid, invitor, invitee and recipient. The NotEqual restriction is used to ensure that the invitee is not the same as the invitor. The output of this is that the recipient is aware that the invitee has been invited by the invitor. The recipient and the invitee can be separate entities as everyone on the network will see the invitation.
Accept Invitation
This rule specifies that if the invitee was the same as the recipient in ReceiveInvite, then the invite is accepted. The invitee sets their state to being invited and more importantly Consents to the FusionID. This rule outputs an accept message.
Receive Accept
This rule is similar to ReceiveInvitation, in that it models how all device’s on the network will observe the message. We have commented out the verification of the accept messages signature to improve the working of Tamarin. This could be a potential area for future research. The output of this rule is that the recipient knows that the invitee has accepted the invite by the invitor.
Send Entrust
When an invitor knows that an invitee has consented to their invitation, is in the fusion ID and knows the fusion secret, the fusion secret is encrypted and sent to the invitee. A State Change is also put on the trace, marking that the invitor knows that the invitee has been entrusted.
Send Proof of Key
This rule processes the encrypted entrust message. It also defines a Proof of Key message, containing an inner and outer signed message. The inner message is signed with the fusion secret to prove knowledge of the key. The signed inner message is then included in the outer message, with is signed with the invitee’s signing key. The state changes in this rule occur for the invitee’s state, where the invitee adds itself to the fusion identity and learns the fusion secret.
Receive Proof of Key
The proof of key message is taken as input. Because we use pattern matching and recreate the same Proof of Key message in the prelude to ReceiveProofOfKey as was done in SendProofOfKey, the message is guaranteed to be signed correctly. The recipient stores receipt of the proof of key in their internal state. This is the final step in all recipients knowing that the invitee is now in the fusion identity.
Send Tombstone
SendTombstone is a simple rule that outputs a signed tombstone message, and sets the internal state of the device sending the tombstone message (the tomber) that the fusion identity has been tombstoned.
Receive Tombstone
The recipient will set the fusion identity to be tombstoned if the sender of the message is in the fusion identity.
Send Redirect
A signed redirect message is output if the sender is in both the old and new fusion identities and the old fusion identity is tombstoned.
Receive Redirect
A redirect message with a valid signature is received if the sender is in both the old and new fusion identities.
Attest Redirect
An attestation of either “accept” or “reject” is modelled. We decided to not model the
nullcase as it was ambiguous. A signed attestation message is output, along with a state change for the attestor of either “accept” or “reject”.Restrictions
dont_invite_members
This restriction prevents tamarin from sending an invite to an invitee if that invitee has already been added to the fusion identity in the invitor’s state.
enforce_not_equal
This restriction prevents two entities from being equal. It is used to ensure that the invitee is not the invitor in ReceiveInvite.
receive_init_only_once
This restriction prevents receiving an init message multiple times. This was necesary to prevent Tamarin from getting caught in endless loops
Lemmas
Fusion Secret Secrecy
Another central security propery of the protocol is that the fusion secret remains secret, as long as none of the members of the fusion id remain honest, i.e. don’t go rogue, lose their device or otherwise leak the key to the adversary.
Roughly, we say that under no circumstances there is a Fusion ID and member thereof, where the adversary knows the key without any member of the Fusion ID losing their device. In Tamarin syntax and using our action facts, this is encoded as follows:
Membership Soundness
A core security property is that nodes don’t get confused about which parties are in the Fusion ID. Only those invited by someone who already is a member should be considered candidates. This lemma proves that for all members that have been added by invitation, there exists someone who was a member before who invited them, or the one they thought they received the invitation from lost their device before. Note that there is one more case: After attaining the fusion secret, the attacker could create another sockpuppet and perform valid invitations from that peer. This rather complex security statement is modelled as follows:
Note the subtle difference between
EntrustSent(in case 3) andStateChange_LearnFusionSecret(in case 2): One fact is emitted when the encrypted entrust message is sent, and one when it is received.Tombstoning Authorization
To ensure that only members of a fusion identity can tombstone the identity, we say that a fusion identity can only be tombstoned if the recipient knows the sender of the tombstone message is in the fusion identity before the tombstone message is receeived, with the exception that the sender could have also lost their device.
Key Is Entrusted Only to Devices that Have Consented to the Fusion Identity
We specify that for an Entruster to entrust another device that the entrusting device has not been lost and the entrusted device has previously consented to the invitation to the fusion identity.
Limitations
Because the redirect and attestation system involves out of band communications and voting methods that cannot be modelled in Tamarin, we were not able to model or provide security proofs on this portion of the protocol.
Observations
The specification was not precise with regards to message format and state transitions. This means that our efforts at modelling the protocol represent our interpretation of the specification and that implementors might have a different interpretation, in which their implementation might diverge from our model (see Issue B).
Additionally, in some instances the modelled protocol slightly deviates from the specified protocol. The main reason for that is that in Tamarin, modelling the referencing of messages by hash is not trivial, which means we didn’t include tangles or other kinds of references in the model. However, if the real protocol messages contain at least all the information as the modelled protocol messages, the security of the real protocol is implied.
Implementation Considerations
Observations
When implementing the protocol, state transitions have to be done according to the protocol spec, or rather the modelled protocol, since the spec is not very precise. Because of the imprecision, we had to interpret a bit during the formal analysis and accordingly the results of the formal analysis do not necessarily translate to other implementations. Since the Scuttlebutt community is diverse, implementations should follow our interpretation to guarantee the security provided in our proofs.
Future Work
Our proposed protocol extension in Suggestion A has not been modelled. Future work could model the extension and guide the design of the protocol extension.
While the Tamarin code was written with best practices in mind, we believe there are still areas that could benefit from refactoring and further scrutiny.
Issues
Issue A: Specification Is Not Precise Enough
We found the specification to be vague with respect to the expected state of the devices when receiving and sending messages, in particular, under which conditions are entities allowed to receive and send messages.
For example, for invite messages the protocol specification states “Only a feed that was either the one that created the fusion identity or has accepted an invite is allowed to create an invite.” While this might guide the implementors of an SSB client, it does not define rules which would restrict the behavior of an attacker. A clearer specification would outline which rules must be satisfied in order to process a received message. These rules would require reference to variables (in pseudocode) that refer to earlier steps in the protocol.
Issue B: No Forward Secrecy
Most if not all modern secure communication protocols provide forward secrecy. This security property describes that encrypted messages sent before a device was corrupted remain secret. In the Scuttlebutt ecosystem, very few components satisfy this notion. We recommend that a forward-secret version of encrypted messages be added.
Suggestions
Suggestion A: Explore Protocol Extension for Authentication for Redirects
After a Fusion Identity has been tombstoned, the protocol specifies a system for publishing redirects. Because at this state of the protocol it is unknown which of the tombstoned fusion identity’s devices can be trusted, a voting system is outlined in the protocol, where users can attest to a redirect. This requires out of band communication for users to verify which redirect is the correct one. While this works for many members of the SSB community that have other means of communicating, for users that are not connected outside the network, this system has drawbacks.
We propose a protocol extension where redirects are authenticated by the individual that generated the original fusion identity. The security of a scuttlebutt identity is based on what a user has, i.e. their private key. For a fusion identity, the secret key of the fusion identity is shared by all devices. In the event that a device is lost or compromised, the security model based on what a user has becomes broken. Because of this, implementing a model based on what the user knows could supplement the redirect process because the user of a compromised device would not know the secret.
The proposed scheme would work as follows: when a user generates a fusion identity, they create a memory based secret (i.e. password), that is passed to a key derivation function and then hashed with a secure hashing algorithm. This hash is then published along with the fusion identity. When the user tombstones their fusion identity and publishes a redirect, the redirect is guaranteed to be authentic because a proof of knowledge of the hash’s preimage (produced by the key derivation function, and not the password itself) is published with the redirect. Because other users can confirm that the redirect is valid by reproducing the hash from the fusion identity initialization, they will know that the redirect was published by the user that created the original fusion identity. This system would allow redirects to be trusted without using any out of band communications or attestation systems.
Suggestion B: There are no Recommendations for how to Protect Private Keys
The protocol operates on the assumption that private keys are maintained private. The security of private keys is then a responsibility for the implementation of the protocol in various clients. Because private keys are stored as regular files on the user’s filesystem without special permissions, it only takes a drive-by browser exploit for a private key to become compromised. We recommend that the protocol outline recommendations for those implementing clients where the key should be stored according to security best practices. For instance, using a secure storage mechanism such as a key chain, or encrypting the private key when at rest.
Appendix
Appendix A: Source Code of Sequence Diagram
The source code can be processed using blockdiag or kroki.io in SeqDiag mode.
Appendix B: Tamarin Source Code