Five Ways Windows Authentication Breaks: A Machine-Checked Tour -- and Why Finding Nothing New Is the Point

1. Was Kerberos Broken, or Did It Just Look Broken?#

In 2014, a domain user could become a domain administrator by changing a single field in a Kerberos ticket ^[1]. Not by breaking any cryptography. The attacker built a Privilege Attribute Certificate that claimed membership in the administrators group, signed it with a checksum that needed no secret key, and handed it to the domain controller. The controller checked the signature, found it valid, read the forged groups, and issued back a ticket carrying full administrative authority ^[1]. Microsoft shipped MS14-068, the hole closed, and the penetration testers moved on ^[2].

The patch fixed the bug. It never answered the question underneath it: was Kerberos broken, or did it just look broken? The whole escalation turned on one mechanism -- whether the controller demanded a keyed signature or accepted an unkeyed checksum. Flip that one switch and the verdict flips with it.

flowchart TD
A[User submits a ticket request with a self-made PAC] --> B{"Does the KDC require a keyed signature on the PAC?"}
B -->|"No, pre-patch"| C[Unkeyed checksum, recomputable by anyone]
C --> D[Forged group memberships accepted]
D --> E[User gains domain administrator authority]
B -->|"Yes, MS14-068 fix"| F[Forged PAC fails verification]
F --> G[Request rejected, privileges unchanged]

Windows runs dozens of authentication protocols, each specified in a Microsoft [MS-*] open specification and each broken, at some point, by its own published CVE. The bulletin recorded MS14-068 only as a privately reported vulnerability and named no discoverer. The widely repeated attribution to Tom Maddock is community folklore, not a vendor confirmation; the bulletin itself says only "privately reported" ^[2]. So here is the question this article answers. I took 23 of those [MS-*] protocols and machine-checked them in the Tamarin prover under one network attacker, each modeled as a flawed version that reproduces its real break and a fixed version that closes it. The result was zero new vulnerabilities -- and that is the finding worth your time.

Three claims, in order. First, the analysis surfaced nothing new: every break it exhibits was already published. Second, nearly every one of those breaks, across protocols that share no code, collapses into just five recurring structural patterns. Third, finding nothing new across a corpus this well-studied is not an anticlimax -- it is the evidence that the five patterns are real and that the protocols, within the model, behave as their specifications claim.

By the end you will have a vocabulary that predicts where an authentication protocol is likely to break before you have read a line of its CVE history. To explain why finding nothing can be a finding, though, we have to back up four decades -- to the first time a machine found a break that every human had missed.

2. Why Anyone Models Protocols at All#

The Needham-Schroeder public-key protocol was published in 1978 and taught as correct for seventeen years ^[4]. Lowe's first attack appeared in 1995 -- seventeen years after the 1978 publication -- with the model-checked break-and-fix following in 1996 ^[5]. The protocol was used, taught, and trusted the entire time -- which is precisely why a machine-checkable method, rather than careful reading, turned out to matter. Then Gavin Lowe pointed a model checker at it and the tool found a man-in-the-middle in an afternoon: an attacker can interleave two runs so that the responder completes believing it authenticated the initiator, when it actually ran with the attacker ^[5]. The attack had been sitting in plain sight the whole time. How did we get a machine that could find what a generation of careful readers had missed?

The answer is a forty-year lineage, and it starts with a precise definition of the enemy. Needham and Schroeder gave the field its genre -- the challenge-response authentication handshake -- and, with it, a habit of arguing informally that a protocol "obviously" works ^[4]. Five years later Danny Dolev and Andrew Yao replaced the hand-waving with a model so pessimistic it became the foundation of everything after it ^[6].

That single abstraction is the load-bearing assumption behind every result in this article, and behind its central limitation. By assuming perfect cryptography, the Dolev-Yao model throws away the bit-level details so it can reason cleanly about message flow -- which is exactly why it sees logic flaws and misses arithmetic ones.

Next came a tool to reason inside the model. Burrows, Abadi, and Needham published BAN logic in 1990, a belief calculus that let analysts write down what each party is entitled to conclude from the messages it sees, layered on top of the Dolev-Yao attacker rather than inventing it ^[8]. BAN made formal reasoning usable. It also showed how a verification method can be confidently wrong.

Then the machines arrived. Lowe's 1996 break used the FDR refinement checker, and his paper did something subtle that turned out to matter for decades: it did not just break the protocol, it fixed it and re-checked the repair ^[5]. Break, patch, prove the patch -- that loop is the direct ancestor of the method in this article. Automated provers followed, in two families ordered by power rather than by date. Lowe's FDR sits at the head of the bounded, finite-state lineage -- explore every protocol run up to a fixed size -- a line later consolidated into toolsets such as AVISPA in 2005 ^[10]. The unbounded symbolic provers, which lift that ceiling to arbitrarily many sessions, were led by ProVerif in 2001 ^[11] and eventually Tamarin in 2013 ^[12]. ※ The split is conceptual, not a timeline: AVISPA (CAV 2005) ^[10] postdates ProVerif (CSFW 2001) ^[11] by four years, and the genuinely earlier bounded exemplar is Lowe's FDR in 1996 ^[5].

Machines find what intuition misses. Lowe's 1996 result was not a cleverer human reading; it was a tool exploring runs a human would never enumerate by hand.

While that method matured, a second, separate history was unfolding inside Windows. The protocols Kerberos, NTLM, CredSSP, LDAP, and their relatives were each specified in a Microsoft [MS-*] document ^{[13] [3]} and each broken, in turn, by its own CVE across more than twenty years -- the breaks Section 4 lays out end to end. The two lineages -- method and application -- ran side by side and barely touched.

flowchart LR
subgraph M["Method lineage"]
M1[Needham-Schroeder 1978] --> M2[Dolev-Yao adversary 1983]
M2 --> M3[BAN belief logic 1990]
M3 --> M4[Lowe and FDR model checker 1996]
M4 --> M5[Unbounded provers, ProVerif 2001]
M5 --> M6[Tamarin 2013]
end
subgraph A["Windows application lineage"]
A1[SMBRelay 2001] --> A2[MS08-068 2008]
A2 --> A3[MS14-068 2014]
A3 --> A4[Relay family 2017-2019]
A4 --> A5[Bronze Bit 2020 and Certifried 2022]
end
M6 --> C[One adversary, whole corpus]
A5 --> C

Lowe broke one protocol and fixed it. The Windows world had dozens, and for two decades each one was broken, and patched, entirely on its own. The first people to point the new machines at these specific protocols could say something rigorous about each -- but only one at a time.

3. One Protocol at a Time#

The machines did get pointed at the protocols Windows actually runs, and the early results were genuinely good. They were also, by construction, local.

Start with public-key Kerberos. PKINIT lets a client authenticate to the Key Distribution Center with a certificate instead of a password, extending the Kerberos V5 service defined in RFC 4120 ^[14]. ※ PKINIT is the public-key front door to Kerberos: it is how smart-card logon ^[15] and Windows Hello for Business ^[16] get an initial ticket. In 2006, Cervesato, Jaggard, Scedrov, Tsay, and Walstad formally analyzed it and found a man-in-the-middle: the KDC's reply was not bound to the requesting client's identity, so an insider could sit between a client and the KDC and make the client accept a session it never established ^[17]. They did not stop at the break. They specified fixes that bind the reply to the client and machine-checked the repair ^[18], with the canonical journal version following in 2008 ^[19]. Break, fix, prove the fix -- Lowe's loop, applied to a protocol shipping in every enterprise.

Two years later, in 2008, Armando, Carbone, Compagna, Cuellar, and Tobarra turned the same lens on SAML 2.0 web-browser single sign-on, the protocol family behind federated login. A missing binding between an assertion and its intended audience let a dishonest service provider redirect a user's authentication to a different one, breaking SSO for Google Apps as their worked example ^[20]. A few years later Cas Cremers re-analyzed IPsec's IKEv1 and IKEv2 and showed cross-mode confusion: properties that hold for one authentication mode can fail once an attacker mixes modes the designers reasoned about separately ^[21].

Underneath two of those results sat one idea that had already been named. In 2003, Asokan, Niemi, and Nyberg described the man-in-the-middle in tunnelled authentication protocols: when an inner authentication runs inside an outer protected channel without being bound to it, an attacker can relay the inner exchange through a channel of its own choosing ^[22]. Their fix was a cryptographic binding between the inner authentication and the protection protocol ^[23] -- the academic root of what Windows would later call channel binding, and the seed of the first of our five patterns.

Each of these was rigorous. Each shipped a real fix that is still in the specifications today. But notice the shape of the work: every analysis built its own model of the attacker, its own idealization of the protocol, its own security goals. PKINIT's adversary was not SAML's adversary, which was not IKE's. So when a practitioner squinted and said "these all feel like the same mistake," that intuition had nowhere rigorous to land. The recurrence was an analogy across papers that did not share a model.

That is the wall the rest of this article is built to climb. Every one of these was a verdict on a single protocol. Nobody had asked, in a checkable way, what the breaks had in common -- because with a different model under each one, nobody could.

4. Twenty Years, the Same Five Mistakes#

Lay the famous Windows-auth breaks end to end and a shape jumps off the page. SMBRelay in 2001, NTLM credential reflection in 2008, the unkeyed Kerberos checksum in 2014, a cluster of relay and channel-binding failures from 2017 to 2019, the Bronze Bit delegation bypass in 2020, the Certifried certificate misissuance in 2022. Different teams, different protocols, different decades -- and a small number of mistakes underneath, repeating.

The first entry is the oldest and the least formal. SMBRelay was demonstrated by the handle Sir Dystic in 2001, and its provenance is an archived Cult of the Dead Cow page rather than an academic paper ^[24]. That archival fragility is itself worth noting: a foundational attack in Windows security history survives mainly as a web-archive snapshot, not a citable primary ^[24]. It showed that an NTLM authenticator, captured on one connection, could be forwarded to a second service that would happily accept it.

timeline
title Windows authentication breaks, 2001-2022
2001 : SMBRelay, NTLM relayed to a second service
2008 : MS08-068, NTLM credential reflection
2014 : MS14-068, unkeyed PAC checksum forged
2017 : CVE-2017-8563, LDAP bind unbound from TLS
2018 : CVE-2018-0886, CredSSP TLS splice
2019 : CVE-2019-1040, drop-the-MIC integrity strip
2020 : CVE-2020-17049, Bronze Bit delegation bypass
2022 : CVE-2022-26923, Certifried misissuance

Every one of these got a fix, and every fix was sound. Channel binding closed the relay and tunnelling failures, formalized for TLS as the bindings in RFC 5929 ^[31]. Requiring a keyed signature closed the forged-PAC escalation ^[1]. Detecting and rejecting a reflected authenticator stopped NTLM credential reflection: MS08-068 changed the way SMB validates authentication replies, so a credential bounced straight back at its sender no longer passes ^[25]. Binding an issued token to its audience and its requester closed the misissuance and redirection failures ^[30]. Protecting a delegation flag with a key closed the Bronze Bit bypass ^[29]. Each repair was correct, shipped quickly, and -- this is the important part -- entirely local to its own protocol.

That locality is the trap. NTLM reflection ^[25] and the unkeyed PAC checksum ^[1] are the same family of mistake -- trusting an integrity value that carries no secret or no direction -- yet they live in protocols that share no code and were fixed years apart by different teams. The relay family of 2017 through 2019 ^{[26] [27] [28]} is one idea, missing channel binding, wearing three protocol costumes. Bronze Bit ^[29] and Certifried ^[30] rhyme with breaks a decade older. The pattern is real, but it is spread across the seams between protocols, exactly where per-protocol work cannot look.

Per-CVE point-fixing is indispensable engineering and a terrible microscope for structure. Each patch is local to one protocol, and each one-protocol analysis rebuilds the attacker model from scratch. So the recurring shape is invisible by construction: you cannot see a cross-protocol pattern one protocol at a time. The fixes were never wrong -- they were just the wrong instrument for the question "what keeps going wrong?"

Which sets up the move the rest of the article depends on. If the shapes are real, you should be able to prove they are real -- not protocol by protocol, but all of them at once, every model facing the same attacker, with the recurrence stated as a checkable claim rather than a feeling. What would it take to build that?

5. One Adversary, One Method, the Whole Corpus#

The move that makes the recurrence checkable is almost embarrassingly simple to state: model 23 of the [MS-*] protocols in a single prover, under one shared attacker, and for each known break build not two models but three. I used the Tamarin prover for this, and its feature list is the reason ^[12].

Tamarin represents a protocol as multiset-rewriting rules over a mutable global state, reasons natively about Diffie-Hellman exponentiation, and verifies properties over an unbounded number of sessions rather than a fixed few ^[12]. It produces both proofs and concrete attack traces, and it has been used on protocols at the scale of TLS 1.3, 5G-AKA, and EMV ^[32]. Windows authentication needs exactly that combination: key exchange with real DH and post-quantum KEMs, credential state that changes as tickets are issued, unbounded concurrent sessions, and the ability to show both that a fix works and that the flawed version breaks. Security goals are written as trace properties.

The third model is the one that turns analogy into evidence.

Here is one lemma, in Tamarin's own property language, for the MS14-068 case -- the claim that only the KDC can produce a PAC a server will accept:

lemma pac_only_kdc_can_sign:
  "All srv pac #i.
       AcceptPAC(srv, pac) @i
   ==> ( Ex #j. KdcSignedPAC(pac) @j & j < i )
     | ( Ex #r. RevealKey('krbtgt') @r )"

Read it as: on every trace, if a server accepts a PAC at time i, then either the KDC actually produced that PAC's keyed signature earlier, or the long-term krbtgt key was revealed ^[33]. In the fixed model, where the integrity check is a keyed signature under krbtgt, Tamarin finds no violating trace and the lemma holds for unbounded sessions. In the flawed model, where the server accepts an unkeyed checksum, Tamarin returns a concrete counterexample -- an acceptance with no prior KDC signature and no key reveal -- which is the forged-PAC escalation, machine-checked ^[1]. The operators and templates are standard Tamarin; the action-fact names are the model's own and are not themselves a citable claim.

Two disciplines keep this honest. The first guards against a lemma that is true only because nothing ever reaches it. A property can be vacuously satisfied if no honest run ever triggers its premise. Non-vacuity sanity lemmas prove an honest party really can complete the protocol, so a "verified" guarantee has teeth rather than being true by absence ^[33]. The second guards against overclaiming: every falsification is matched to a published CVE or paper before I call it a reproduction. Nothing in this corpus is presented as a discovery.

flowchart TD
P[One protocol, one Dolev-Yao adversary] --> F[Fixed model, mechanism present]
P --> X[Flawed model, one mechanism removed]
P --> K[Control model, mechanism re-enabled]
F --> FR[Security lemma verifies]
X --> XR[Same lemma falsifies, the published break]
K --> KR[Same lemma verifies again]
FR --> D{"Did only the toggled mechanism move the verdict?"}
XR --> D
KR --> D
D -->|Yes| C[Cause localized to the mechanism, not the harness]

The control model is the difference between a story and a proof. Without it, "these breaks are all the same pattern" is a nice grouping of war stories. With it, the claim becomes machine-checked and specific: toggle this one mechanism and the security property flips, restore it and the property returns. The recurrence is no longer an analogy across papers -- it is a falsifiable statement about a mechanism, repeated across protocols that share no code.

Finding nothing new across a well-studied corpus is not a null result. It is the evidence that the taxonomy is real -- the protocols behave, within the model, exactly as their fixes claim.

With the instrument built, the corpus gives up its structure without much further argument. There are five shapes. Here is each one, with the worked break behind it.

6. The Five Patterns#

Before you read a single CVE, ask five questions of any authentication protocol. Each question targets one of the recurring shapes, and a "no" to any of them names the family of break to expect. This decision tree is the article's centerpiece -- the audit you can run from memory.

flowchart TD
S[Any authentication protocol] --> Q1{"Is every authenticator bound to the channel and endpoint it is used on?"}
Q1 -->|No| P1[Pattern 1, relay and MITM]
Q1 -->|Yes| Q2{"Is every integrity check keyed, never a bare checksum?"}
Q2 -->|No| P2[Pattern 2, keyed-vs-unkeyed confusion]
Q2 -->|Yes| Q3{"Does every symmetric credential carry a direction or role tag?"}
Q3 -->|No| P3[Pattern 3, credential reflection]
Q3 -->|Yes| Q4{"Does every signed token bind requester, key, and audience?"}
Q4 -->|No| P4[Pattern 4, identity-binding gap]
Q4 -->|Yes| Q5{"Does every delegation chain keep its restriction under composition?"}
Q5 -->|No| P5[Pattern 5, delegation and composition]
Q5 -->|Yes| OK[No break in these five shapes within symbolic reach]

Pattern 1: Missing or ignored channel binding#

The first pattern is the relay. An authenticator -- an NTLM response, a signed bind, a delegated credential -- is computed without naming the channel it is supposed to travel on, so an attacker can carry it to a different service that will accept it just the same. This is the modern form of the tunnelled-authentication man-in-the-middle that Asokan, Niemi, and Nyberg described in 2003 ^[22].

The worked model is NTLM. With no channel binding, a victim's NTLM exchange relays cleanly to a second service ^[13]; add the binding and the relayed authenticator no longer matches the channel it arrives on, and the target rejects it.

sequenceDiagram
participant V as Victim client
participant M as Attacker relay
participant T as Target server
V->>M: Connect, NTLM NEGOTIATE
M->>T: Relay NEGOTIATE as the victim
T->>M: NTLM CHALLENGE, server nonce
M->>V: Forward the same CHALLENGE
V->>M: NTLM AUTHENTICATE over the nonce
M->>T: Relay AUTHENTICATE unchanged
Note over M,T: No channel binding, so the target cannot tell the response came from a different connection
T->>M: Access granted as the victim

The same shape recurs across protocols that share no code. CredSSP failed to bind its pubKeyAuth value to the TLS session, so a man-in-the-middle could splice itself into an RDP credential handshake ^[27]. LDAP accepted a bind without tying it to the TLS channel underneath, and Microsoft's own documentation is blunt that the default performed no channel-binding validation at all ^{[37] [26]}. The companion guidance spells out the man-in-the-middle risk ^[38] under the umbrella advisory for LDAP hardening ^[36]. And drop-the-MIC removed NTLM's integrity check without invalidating the surrounding signature. drop-the-MIC strips the NTLM message-integrity check from the negotiated flags without invalidating the outer signature, so a tampered exchange still verifies as authentic ^[28].

The fixes are all the same idea wearing different names: the TLS channel bindings tls-server-end-point and tls-unique defined in RFC 5929 ^[31], and the SPNEGO mechListMIC that stops a negotiation downgrade ^[39]. One subtlety decides whether the fix actually closes the door. RFC 5929's tls-server-end-point hashes the server certificate, so it is per-certificate, not per-service. Two services sharing one certificate share one binding value -- which is exactly the gap that kept some LDAP deployments relayable even after binding was nominally enabled ^[31].

Pattern 2: Keyed-vs-unkeyed integrity#

The second pattern is a confusion between two things that look alike and behave nothing alike: a checksum and a keyed signature.

This is MS14-068 exactly. The KDC accepted a PAC whose integrity "signature" could be an unkeyed checksum, so a user could forge group memberships and compute a matching checksum themselves ^[1]. Require that the PAC carry a keyed signature under the krbtgt key, and the same forgery fails because the user cannot produce the tag ^[2]. The identical class shows up at the server-to-domain-controller PAC validation step, where a service asks a DC to vouch for a ticket's PAC ^[3]. The fix and the failure are one mechanism, toggled.

// A toy checksum: no secret, so anyone can recompute it over any data.
function checksum(data) {
let sum = 0;
for (const ch of data) sum = (sum + ch.charCodeAt(0)) % 65521;
return sum;
}
// A toy keyed tag: the value depends on a secret the attacker does not hold.
function tag(key, data) {
let acc = key.length * 131;
for (const ch of (key + data)) acc = (acc * 31 + ch.charCodeAt(0)) % 1000003;
return acc;
}

const forged = "groups=domain-admins";

// Unkeyed: the attacker computes the same checksum the verifier will recompute.
const attached = checksum(forged);
const verifier = checksum(forged);
console.log("unkeyed checksum accepts forged data:", attached === verifier); // true

// Keyed: without the KDC secret, the attacker cannot match the expected tag.
const kdcSecret = "krbtgt-secret";
const serverExpects = tag(kdcSecret, forged);
const attackerTag = tag("no-secret", forged);
console.log("forged keyed tag accepted:", attackerTag === serverExpects); // false

Pattern 3: Symmetric-credential reflection#

The third pattern is reflection. A credential computed by a keyed function that carries no direction or role tag can be bounced back at the party that produced it. The canonical Windows instance is NTLM credential reflection, fixed in MS08-068 ^[25]: an attacker who receives a victim's challenge-response can send that same authenticator back to the victim's own machine and be accepted as the victim ^[34]. It sits in the SMBRelay lineage that opened our timeline ^[24].

The toggle is a direction tag. Remove it and the value a client produces is exactly the value a server will accept, so the reflection works. Restore a role offset -- so the two directions compute different values -- and the reflected response no longer matches.

// A symmetric response: both ends compute the same function of nonce and key.
function respond(key, nonce, role) {
let acc = 0;
for (const ch of (role + key + nonce)) acc = (acc * 33 + ch.charCodeAt(0)) % 1000003;
return acc;
}

const key = "shared-session-key";
const nonce = "server-nonce-1234";

// No direction tag: what a client sends equals what a server would accept.
const clientSends = respond(key, nonce, "");
const serverAccepts = respond(key, nonce, "");
console.log("reflected response accepted, no tag:", clientSends === serverAccepts); // true

// With a direction tag, the two directions diverge and reflection fails.
const clientTagged = respond(key, nonce, "client-to-server");
const serverTagged = respond(key, nonce, "server-to-client");
console.log("reflected response accepted, tagged:", clientTagged === serverTagged); // false

There is one place this pattern is easy to overclaim, and the honesty frame of this whole article depends on not doing so. In my Tamarin model of [MS-NRPC], a client may pick its Netlogon NetrServerAuthenticate3 challenge to coincide with the server's -- a structural reflection the symbolic model can express. This is a modeling observation, not a separately published Netlogon weakness; the famous Zerologon escalation turns on the computational AES-CFB8 zero-IV weakness that a perfect-crypto model cannot represent. Zerologon appears here only as the Section 9 boundary illustration -- encoded as an equation, never discovered ^[40].

Pattern 4: Identity-binding gaps in signed tokens#

The fourth pattern is a signed thing -- a reply, a ticket, an assertion, a certificate -- that is correctly signed and yet fails to bind who it is for. PKINIT is the textbook case: the KDC's reply was not bound to the requesting client's identity, the gap Cervesato and colleagues formalized ^[19]. In Diffie-Hellman mode this becomes an unknown-key-share risk, where a client can be steered into misattributing a key. The fix binds the request itself with the paChecksum defined in RFC 4556 Section 3.2.1, a checksum over the request body ^[35]. RFC 8636 later made its hash negotiable under "paChecksum Agility" -- it did not add the field, it standardized the field's agility ^[41].

The same gap appears wherever a token crosses a trust boundary. SAML single sign-on needed an audience restriction so an assertion minted for one service could not be redirected to another ^[20]. AD CS certificate enrollment needed the issued certificate's subject bound to the requester's real identity -- absent that, the Certifried technique let a low-privilege account enroll a certificate for a domain controller ^[30], a later escalation across the AD CS attack surface that SpecterOps's Certified Pre-Owned had first mapped in June 2021 ^[42]. OAuth's on-behalf-of exchange needs its token audience checked to avoid a confused-deputy redirection ^[43], and device registration needs a proof-of-possession binding so a bearer token cannot be replayed against a key the device never held ^[44].

Pattern 5: Delegation and composition#

The fifth pattern is the subtlest, because every component is sound on its own. The failure lives in the chain. Kerberos constrained delegation lets a service act on a user's behalf, gated by whether a ticket is marked forwardable. The Bronze Bit technique flipped that restriction: a compromised service could tamper with a service ticket that was not valid for delegation and force the KDC to accept it, because the relevant integrity was not protected by the KDC's own ticket signature ^[29]. Restore the check on the krbtgt ticket signature and the tampered ticket is rejected ^[45].

Composition multiplies the surface. Resource-based constrained delegation chains can be assembled into escalation paths that no single hop authorizes ^[46]. A cross-protocol NTLM relay shares one credential across SMB, LDAP, and CredSSP at once, so a binding omitted in any one leg reopens the whole composition. And IKE's cross-mode confusion is a composition failure at the key-exchange layer, where mixing modes defeats a property each mode satisfies alone ^[21].

Every pattern so far is a way something broke. But the instrument that exhibits a break can also prove a guarantee -- and when I pushed twelve of these models under stronger attackers, what came back was not new bugs but stronger proofs. What did the deep models actually prove?

7. What the Deep Models Proved#

A prover does not only produce counterexamples. When a lemma holds, you get a proof -- a statement that across every run, under this attacker, nothing violates the property. So I took twelve of the models and deepened them: same protocols, stronger attacker. The headline stayed the same. No new breaks. What changed is that the guarantees got stronger, and I can say precisely which attacker capability each one now survives. Everything below is my Tamarin verification within the Dolev-Yao model, each item anchored to the public specification or CVE it concerns -- not an independently published finding.

The deepenings follow a single recipe: add an attacker capability the per-protocol models had assumed away, then see which lemma still holds.

A few deserve a sentence. PKINIT's public-key-encryption mode structurally cannot offer forward secrecy, because the reply key arrives encrypted to a long-term key; the DH mode can, and the deepened model proves it does even when both signing keys leak after the run ^[35]. The hybrid post-quantum result is the strongest-sounding and has no public primary, so I flag it as model-only: binding the KEM ciphertext into the transcript keeps a client's acceptance tied to the genuine server even when both the classical and post-quantum legs are revealed. The delegation result matters most operationally: a Protected Users account is never delegated by any path -- classic, resource-based, or PKINIT-issued -- even under arbitrary service-key compromise ^[47].

Honesty requires one scar on this table. One deepening did not yield an independent re-proof in my sandbox. The heaviest cross-domain four-signature-PAC model exhausted memory -- an out-of-memory EXIT 137 -- before Tamarin terminated. I record that result as reported, not independently re-proved ^[3]. A guarantee I cannot re-derive is a guarantee I report with an asterisk, not one I assert.

These proofs are strong, but they are exactly as strong as the model they live in -- no stronger. So the fair next question is how Tamarin compares with the other instruments on the bench, and, more pointedly, what it is choosing not to see.

8. Symbolic, Computational, and the Tools Between#

Tamarin was the right instrument for this corpus, but it is one of several, and the honest comparison is about what each one buys and what it costs. The computer-aided cryptography community's own survey lays out the taxonomy, and I follow it here ^[7].

The first split is the model. Symbolic tools -- Tamarin, ProVerif, Scyther -- work in the Dolev-Yao world of perfect cryptography and reason about protocol logic. Computational tools -- CryptoVerif, EasyCrypt -- model the attacker as a probabilistic polynomial-time algorithm and produce bounds on its success probability ^[7]. They answer different questions, which is why a single benchmark number rarely transfers between them.

Why Tamarin for Windows authentication, then? Because these protocols need Diffie-Hellman and post-quantum KEMs, credential state that mutates as tickets are issued, unbounded sessions, and both proofs and concrete attack traces in one tool ^[12]. ProVerif is often faster, but its Horn-clause over-approximation makes stateful DH flows awkward and can surface attacks that do not really exist ^[48]. Scyther guarantees termination, but only on a restricted protocol class that this corpus repeatedly steps outside of ^[49]. The pattern-refinement technique behind Scyther is worth reading in its own right ^[53].

Could a symbolic proof simply hand off to a computational guarantee? Sometimes, and that bridge has a name.

So the bridge is real but partial, which is why the survey's recommendation is not "pick the best tool" but "combine them": symbolic for protocol logic at scale, computational for primitive strength, and a third layer for the code ^[7]. That third layer is the active frontier. DY* embeds Dolev-Yao symbolic analysis as a library for executable F* code and used it to mechanize Signal end to end, closing the gap between a model and the program that ships ^{[56] [57]}. Verifpal trades some expressiveness for a gentler modeling language with formal semantics, aiming to lower the rate of modeling mistakes ^[58].

Every one of those tools, the symbolic ones especially, shares a single blind spot. It is not a defect in any implementation. It is the definition of the model itself -- and it is where this article has been heading all along.

9. The Boundary the Method Cannot Cross#

Return to the question from the first paragraph: was Kerberos broken, or did it just look broken? The honest answer is that a perfect-crypto model can prove a protocol's logic sound and still be completely blind to a flaw that ships a domain takeover. Two results make that boundary precise, and neither is a defect you could engineer away.

The first is about decidability. Durgin, Lincoln, Mitchell, and Scedrov showed that secrecy for protocols with an unbounded number of sessions is undecidable ^[59]. Restrict to a bounded number of sessions and the problem becomes "merely" NP-complete, as Rusinowitch and Turuani proved ^[60]. Put those together and you get a hard fact about tooling: no symbolic verifier can be simultaneously sound, complete, and guaranteed to terminate. Each tool gives up one. Tamarin may not terminate; ProVerif sacrifices completeness and can report false attacks; Scyther restricts the protocol class it accepts ^[7].

The second boundary is sharper, and it is the heart of the whole article. The Dolev-Yao model abstracts cryptography to perfect operations, so it provably cannot represent a flaw that lives in the cryptographic arithmetic itself. Zerologon is the flagship example. The Netlogon credential used AES in CFB8 mode with an all-zero initialization vector, and with probability $\approx 1/256$ per attempt an all-zero plaintext produced an all-zero ciphertext, letting an unauthenticated attacker forge the credential and ultimately seize a domain controller ^[40]. The mechanism is laid out in the disclosure whitepaper ^[61]. No symbolic model sees this, because the model has no notion of an IV, a block-cipher mode, or a $1/256$ probability. There is nothing to find.

flowchart TD
F[A protocol failure] --> Q{"Is it in the message logic or in the cryptographic arithmetic?"}
Q -->|Message logic| S[Symbolic model sees it: relay, reflection, missing binding, signature confusion]
Q -->|Cryptographic arithmetic| C[Symbolic model is blind: zero-IV, weak hash, probability gaps]
C --> Z[Zerologon lives here, encoded as an equation, never discovered]
S --> V[Tamarin can verify or falsify]

This is why the article has been so insistent about one phrase. Where the corpus shows a computational consequence, it encoded the published weakness as an equation in the model; it did not find it.

The boundary is the result, not a failure. Unbounded verification is undecidable, and a perfect-crypto model provably cannot represent a probabilistic flaw. So "nothing new across a well-studied corpus" is not an anticlimax. It is the model telling you, precisely, that the protocol logic is sound and that whatever risk remains must live one layer down. That is the most useful thing a symbolic prover can say -- and it can only say it honestly if you respect the wall.

Verified means: within this model, against this adversary, no trace violates this property. Nothing more, and nothing less.

The boundary also tells you which famous attacks were never in scope to begin with.

If the boundary is permanent -- and it is -- then the most interesting questions live right up against it. Where does the method, and this particular corpus, still strain?

10. Where the Method Still Strains#

The boundary is not the end of the work; it is where the hardest open problems begin. Five of them bound this corpus.

Computational soundness at full-protocol scale. The dream is to lift a symbolic proof of a deployed protocol automatically to a computational guarantee covering the real primitives -- exactly the gap that hides Zerologon-class flaws. Soundness theorems exist, but only for restricted primitives and conditions ^[54]. The working answer today is the survey's layered stack -- combine symbolic, computational, and code-level tools -- not a universal bridge ^[7].

Termination with full algebraic theories. Tamarin reasons about Diffie-Hellman and exclusive-or, but with those theories it may not terminate, and terminating results exist only for restricted equational fragments such as Scyther's class. The undecidability wall keeps this an open trade between expressiveness and automation ^[59].

Composition and whole deployments. Composition theorems are provable for specific seams -- per-channel bindings survive a shared-credential relay, for instance. But scaling to a whole interacting deployment is unsolved, and this corpus hit the wall directly: the heaviest cross-domain four-signature-PAC model exhausted memory on independent re-proof, a concrete state-explosion failure rather than a theoretical one ^[21].

Privacy and equivalence at scale. Secrecy and authentication are reachability properties. Privacy properties -- unlinkability, anonymity -- are equivalence properties, which are markedly harder and scale worse. Tamarin's observational equivalence and ProVerif's equivalence checking handle modest protocols, but the frontier here is genuinely hard ^[7].

From verified models to verified deployments. A proof about a model is only as good as the model's fidelity to the running code. DY* mechanized Signal end to end from executable F* code ^[56], and Verifpal lowers the modeling-error rate with friendlier semantics ^[58]. But [MS-*] implementations are closed, so for this corpus model fidelity has to be argued from the public specification rather than mechanically derived from the binaries.

Those are the frontier's problems, and none of them has to be solved before the five patterns become useful. Here is what you can do with them this afternoon.

11. Auditing With the Five Patterns#

The taxonomy earns its keep as a checklist. You do not need Tamarin to use it -- you need a specification, a design review, and five questions. Each maps to a concrete Windows mechanism and a documented fix.

A "no" to any question does not prove a break -- it tells you where to look first, and which published fix already exists. That is the difference between a taxonomy and a vulnerability scanner: the taxonomy makes you faster at the questions, not lazier about the answers.

If you go further and model a protocol yourself, the corpus's method carries two warnings worth repeating.

Run those five questions and you are doing by hand what the corpus did by machine. Which leaves only the questions people ask out loud when they hear the phrase "I verified Windows authentication and found nothing."

12. Questions People Ask#

So: was Windows authentication broken, or did it just look broken? The answer the corpus gives is precise. Twenty-three protocols, one adversary, twelve of them pushed harder -- and every break it could exhibit was one already on the record, each reducible to one of five structural shapes: a missing channel binding, an unkeyed integrity check, an untagged symmetric credential, an unbound token, or a restriction that dissolves under composition. The same models that exhibit those breaks also prove the fixes hold, even when you hand the attacker more power than the original analyses dared.

The shapes themselves are old news. Channel binding, keyed integrity, direction tags, audience binding, and delegation protection were each understood when they were each invented. What was missing was a way to say, in one breath and with a machine to back it, that they are the same five mistakes recurring across protocols that share no code -- and to draw the line, exactly, where a symbolic prover stops seeing and Zerologon's arithmetic begins.

That line is the gift. It tells you that "nothing new" is not the tool shrugging; it is the tool reporting, honestly, that the logic is sound and the remaining risk lives one layer down. Carry the five questions with you. The next authentication protocol has not been written yet -- but when it is, you already know the five ways it is most likely to break.