# 🔐 `skyauth`
[](https://crates.io/crates/skyauth)
[](https://docs.rs/skyauth)
[](LICENSE-MIT)
[](src/lib.rs)
> **Pure Safe Rust (`#![forbid(unsafe_code)]`), Zero-Panic AT Protocol OAuth 2.1 Client with RFC 9449 DPoP, RFC 9126 PAR, RFC 7636 PKCE, & Formal Mathematical Verification**
---
## 🌟 Highlights
- **100% Pure Safe Rust**: `#![forbid(unsafe_code)]` enforced crate-wide with 0 `unsafe` blocks and zero production panics.
- **RFC 9449 DPoP**: Ephemeral ECDSA P-256 key generation, RFC 7517 JWK formatting, RFC 7638 JWK Thumbprints (`jkt`), signed `dpop+jwt` proof tokens, access token hash (`ath`), and transparent auto-nonce retry negotiation.
- **RFC 9126 PAR (Pushed Authorization Requests)**: Direct back-channel pushing of authorization parameters with signed DPoP headers.
- **RFC 7636 PKCE**: High-entropy 43-character Base64URL verifier generation, SHA-256 S256 challenge derivation, and constant-time verification.
- **Decentralized Identity Discovery**: Handle normalization, DNS TXT resolution (`_atproto.<handle>`), HTTPS fallback (`/.well-known/atproto-did`), DID resolution (`did:plc`, `did:web`), and bidirectional `alsoKnownAs` verification.
- **RFC 8414 & RFC 9728 Discovery**: Protected Resource Metadata and Authorization Server Metadata discovery with automatic OIDC fallback.
- **Strict SSRF & DNS Rebinding Security**: Full IP boundary filtering blocking RFC 1918 private IPs, loopback, link-local, cloud metadata (`169.254.169.254`), IPv6 ULA, and DNS socket pinning.
- **64-Shard Partitioned State Store**: Lock-free scaling state storage across 64 independent `RwLock` shards with atomic single-use state consumption ([`OAuthStore::take_state`]) and drift-free background TTL pruning.
- **Web Framework Integrations**: Ready-to-use extractors, response generators, and middleware for **Axum 0.7**, **Actix-Web 4**, and **Tower**.
- **Formal Mathematical Verification**: Verified using **Verus** deductive proofs, **Kani** bounded model checking with 25 mandatory anti-vacuity reachability tags enforced across 5 proof harnesses, and pure-Rust executable state transition models.
- **Confidential Client Support**: Automatic `client_secret` inclusion in PAR, code exchange, and refresh requests (RFC 6749 § 2.3.1 `client_secret_post`); extensible credential hook via `execute_par_request_with_credentials`.
- **Proxied-Deployment DPoP**: `with_htu_override` on the Tower layer reconstructs absolute DPoP target URIs for servers behind reverse proxies receiving origin-form request targets.
- **Hardened SSRF Boundary**: Deprecated 6to4 (`2002::/16`, with embedded-IPv4 re-evaluation) and Teredo (`2001::/32`) tunneling prefixes are blocked, mirrored in the formal verification models; test mode (`allow_insecure_localhost`) only exempts explicit loopback targets, never metadata/internal hosts.
- **Single-Use Server Nonces**: Optional strict RFC 9449 § 8 nonce consumption (`InMemoryServerNonceSource::with_single_use`).
- **Resource-Server Token Validation**: `JwtAccessTokenValidator` (RFC 9068 `at+jwt` verification with fail-closed issuer/audience matching and `cnf.jkt` DPoP binding) and an in-memory registry, with a Tower middleware layer enforcing DPoP proof verification, replay rejection, and server nonce challenges.
- **XRPC Client Hardening**: Lexicon NSID grammar validation on `send_xrpc_request`, DPoP-signed requests with automatic nonce retry, and bounded response bodies.
- **Dynamic Schema Invariants**: Bundled official ATProto Lexicons and RFC schemas with continuous automated upstream drift detection.
---
## 🚀 Quick Start
Add `skyauth` to your `Cargo.toml`:
```toml
[dependencies]
skyauth = "0.2"
```
### 1. DPoP Proof Generation & Verification
```rust
use skyauth::dpop::{compute_access_token_hash, DPoPKey, DPoPVerifier};
use skyauth::pkce::PkcePair;
fn main() -> Result<(), Box<dyn std::error::Error>> {
// 1. Generate PKCE code challenge
let pkce = PkcePair::generate();
assert_eq!(pkce.verifier.len(), 43);
// 2. Generate ephemeral DPoP keypair
let dpop_key = DPoPKey::generate();
let _jkt = dpop_key.jwk_thumbprint();
// 3. Create a DPoP proof for an outgoing token request
let proof = dpop_key.create_proof(
"POST",
"https://pds.example.com/oauth/token",
None,
None,
)?;
// 4. Verify inbound DPoP proof
let verifier = DPoPVerifier::new();
let (claims, _jwk) = verifier.verify_proof(
&proof,
"POST",
"https://pds.example.com/oauth/token",
None,
None,
None,
)?;
assert_eq!(claims.htm, "POST");
Ok(())
}
```
### 2. Full OAuth Client Lifecycle
```rust
use skyauth::client::{AtprotoOAuthClient, CallbackParams, OAuthClientMetadata};
use skyauth::store::OAuthStateStore;
use std::sync::Arc;
use std::time::Duration;
#[tokio::main]
async fn main() -> Result<(), Box<dyn std::error::Error>> {
// 1. Configure OAuth Client Metadata
let metadata = OAuthClientMetadata::new(
"https://my-app.example.com/client-metadata.json",
"https://my-app.example.com/oauth/callback",
)
.with_client_name("My ATProto App")
.with_scope("atproto transition:generic");
// 2. Instantiate high-level client with 64-shard concurrent state store
let state_store = Arc::new(OAuthStateStore::new(Duration::from_secs(300)));
let client = AtprotoOAuthClient::builder()
.metadata(metadata)
.state_store(state_store)
.state_ttl(Duration::from_secs(300))
.build()?;
// 3. Initiate login with handle or DID (pushes PAR, generates PKCE, registers state)
let auth_req = client.authorize("alice.bsky.social").await?;
println!("Redirect user to: {}", auth_req.authorization_url);
// 4. Handle incoming callback after user authorization (single-use consumed)
let callback_params = CallbackParams::new("auth_code_from_query", &auth_req.state)
.with_iss("https://bsky.social");
let session = client.handle_callback(&callback_params).await?;
println!("Authenticated user DID: {}", session.sub);
// 5. Execute authenticated XRPC request
let response = client
.send_xrpc_request(&session, "com.atproto.repo.describeRepo", &[])
.await?;
println!("XRPC response status: {}", response.status());
Ok(())
}
```
---
## 🛡️ Formal Verification & Mathematical Invariants
`skyauth` incorporates a multi-layered formal verification hierarchy:
1. **Verus Deductive Contracts (`verus!`)**: Deductive mathematical proofs in [`src/verification/verus_contracts.rs`](src/verification/verus_contracts.rs) using SMT solving (Z3) to prove single-use state transition safety, terminality, SSRF IP range isolation, and PKCE bounds.
2. **Kani Bounded Model Checking (`kani::proof`)**: Exhaustive symbolic proof harnesses in [`src/verification/kani_harnesses.rs`](src/verification/kani_harnesses.rs) using symbolic `kani::any()` and `kani::assume()` inputs with 25 mandatory anti-vacuity reachability tags (`kani::cover!` / [`AntiVacuityCoverage`]) that the deterministic test suite must reach.
3. **Executable Formal State Models**: High-assurance transition models in [`src/verification/formal_models.rs`](src/verification/formal_models.rs) tested against property fuzzing and concurrent interleavings.
---
## 🧪 Running Tests, CI & Formal Proofs
```bash
# Run unit, integration, and RFC vector test suites
cargo test --all-targets --all-features
# Verify strict clippy compliance (0 warnings)
cargo clippy --all-targets --all-features -- -D warnings
# Verify specification drift against upstream canonical Lexicons & RFC schemas
bash scripts/sync_specs.sh --verify
# Run Kani bounded model checking proof harnesses
cargo kani --harness proof_
# Run Verus deductive formal verification proofs
bash scripts/run_verus.sh
```
---
## 📄 License
Dual-licensed under either:
- **MIT License** ([LICENSE-MIT](LICENSE-MIT))
- **Apache License, Version 2.0** ([LICENSE-APACHE](LICENSE-APACHE))