Security
Miko pairing and end-to-end encryption
Abstract
Miko separates the services that route a connection from the endpoints that read its contents. A client device and the machine running the user's work (the Host) establish their own encrypted channel. The relay carries that channel without receiving its decryption secrets. Pairing establishes which Host belongs to an account; device approval establishes which client devices may act for that account.
This paper describes those mechanisms and the properties established by Miko's internal symbolic verification. The central confidentiality result is precise: under the model's assumptions, an attacker controlling the relay and control plane cannot recover protected channel content. The Host remains an endpoint that processes that content. This is a protocol result under stated assumptions, not a proof of every part of the product.
Establishing trust
Connecting a machine
Connect pairing begins with a code generated on the client device and transferred privately by the person to the Host. The two endpoints use CPace, a password-authenticated key exchange, to establish a shared secret over an otherwise untrusted relay. Neither observing nor interfering with the exchange gives an offline test for guesses of the code.
The endpoints then exchange encrypted identity information. The account's signing authority authorizes the Host, and the Host checks that authorization against the account identity and trust history established during pairing. Completion depends on those cryptographic checks. A relay's report that pairing has finished is insufficient on its own.
The Connect guarantees depend on the code reaching the intended Host privately. A Miko Cloud machine is set up differently: Miko's provisioning service delivers the code to the new machine, so it takes part in establishing that endpoint. The Connect results in this paper assume a privately transferred code and do not cover that hosted setup.
Approving another device
An existing trusted device approves a new device through a short-code comparison. A commitment fixes the new device's identity and requested authorization before the comparison challenge is revealed. The person compares the displayed codes on both devices. The existing device signs the authorization; the new device checks that the authorization names its own identity and, where applicable, its requested expiry.
The verified protocol binds the approval to the identity and authorization being compared. Its assumptions include an authentic comparison by the person. The symbolic analysis does not provide a numerical estimate of the chance of guessing a short displayed code.
Protecting a connection
After trust is established, the client and Host use a Noise IK channel. The handshake authenticates their cryptographic identities and derives session secrets. Authenticated encryption protects channel content, while the protocol binds accepted transport messages to their sender and session. The Host's admission check connects cryptographic identity to authorization.
The verification distinguishes handshake traffic, confirmed transport traffic and later key updates. Its forward-secrecy results cover confirmed transport traffic: the device's messages, and the Host's messages after the device's first message, stay protected even if both long-term identity keys are disclosed after the session. In the modeled key update, messages sent before the update stay protected if a later key is disclosed.
Who can see what
| Participant | Visibility and responsibility |
|---|---|
| Authorized client device | Reads the content it displays and creates the actions it sends. Its software and local security are part of the endpoint trust boundary. |
| Host | Decrypts and processes the user's work. End-to-end encryption does not conceal content from this execution endpoint. |
| Relay and control plane | Handle routing and account/device associations and can observe traffic timing and size. Once the client trusts the Host's keys as described above, they cannot decrypt protected channel content or forge accepted authenticated transport messages. |
| A service intentionally used by the work running on the Host | Receives the content that work sends to it. Protection of the client-to-Host channel does not establish confidentiality from such a recipient. |
Encryption does not hide all metadata or guarantee availability. A malicious relay can delay or suppress traffic. The confidentiality claims also assume trusted endpoint software, protected endpoint secrets and the intended trust establishment; they do not establish security against compromise of an endpoint.
What the models prove
The models give an active attacker control over the communication network, including interception, modification, replay and concurrent sessions. Cryptographic primitives are modeled as ideal operations. Within those assumptions, the proved properties include:
- Connect pairing confidentiality: the relay cannot obtain the code, the shared secret, the keys derived from it or the Host's name sent in the encrypted exchange, and cannot test code guesses offline.
- Connect identity agreement: a completed binding agrees on the account and Host identities authorized by the participating endpoints.
- Device approval agreement: acceptance is tied to the approving device's authorization of the new device's own identity and requested expiry.
- Channel confidentiality and authentication: the modeled protected payloads remain secret, and accepted transport messages correspond to authenticated sends, subject to the explicitly modeled compromise conditions.
- Transport and admission safeguards: confirmed transport traffic has forward secrecy; a replayed first handshake message yields no session key and never counts as a connected device; and the modeled admission rule excludes an identity already marked revoked and prevents an authorized attacker from claiming a different device's identity.
The admission result assumes the Host has the modeled authorization state. It is not a claim about how quickly a distributed system learns a revocation.
Verification record
The pairing campaign was checked with ProVerif 2.05 on 17 October 2026. It comprised 17 model runs and 65 query outcomes, all matching their expected outcomes. It covers Connect pairing, device approval, restore approval and Preview authorization, together with deliberately altered models and other comparison runs.
Within that campaign, the three current Connect and device-approval model runs produced 15 proved security queries and five successful reachability checks. All 20 achieved their intended results. Reachability checks demonstrate that honest executions can complete; they are separate from security proofs. Negative controls deliberately remove protections or change assumptions and are expected to expose attacks. Agreement with an expected outcome is not synonymous with a proved security guarantee.
The channel record uses ProVerif 2.05 and Noise Explorer 1.0.7, dated 16 October 2026. Two unmodified Noise IK reference models produced 37 verdicts each, matching the reference results in all 74 comparisons. Miko's channel model contains 25 queries; its base-model results include 16 proved security queries. The channel claims above are drawn from successful proofs and retain their compromise assumptions. These counts describe separate verification sets and should not be added into a single count of product guarantees.
The models were developed from the implementation for internal review. They establish protocol properties within their abstractions; they do not replace implementation testing or independent cryptographic review.
Security researchers can request the full models at contact@getmiko.app.