AI导哈

信号协议模型上下文协议服务器

一个经过形式验证的模型上下文协议（MCP）服务器，为大型语言模型集成提供Signal协议的加密操作。

  • by bmorphism
  • Rust
  • 本地部署
  • 更新于
在 GitHub 查看 bmorphism/signal-mcp

使用说明

Signal MCP：用于信号协议的模型上下文协议服务器

一个经过正式验证的模型上下文协议（MCP）服务器，为LLM集成公开信号协议加密操作。

🌟 主要特点

  • 17结构线形 MCP原语与信号协议之间
  • 形式验证 通过Coq证明义务（根据 .topos/)
  • 代表团运作 操作组合架构
  • BDD+依赖类型 用于行为规范
  • 平衡三元种子1069: [+1, -1, -1, +1, +1, +1, +1]

🏗️ 建筑

MCP资源（只读状态）

  • signal://sessions/{addr}/{device} -双棘轮会话状态
  • signal://identities/{service_id} -身份密钥（Curve25519）
  • signal://messages/{conv}/{msg} -消息历史记录
  • signal://groups/{id}/credentials -zkgroup凭据

MCP工具（状态操作）

  • signal_encrypt_message -双棘轮+密封发件人加密
  • signal_decrypt_message -密封发件人拆封+解密
  • signal_initialize_session -X3DH密钥协议
  • signal_verify_safety_number -指纹验证
  • signal_generate_group_auth -零知识组证书
  • signal_multi_recipient_encrypt -正在进行批量加密

MCP提示（LLM工作流）

  • signal_secure_conversation_starter -语境信息构成
  • signal_group_privacy_audit -隐私态势分析
  • signal_safety_number_change_alert -安全教育
  • signal_device_linking_guide -多设备设置
  • signal_backup_restore_wizard -云备份用户体验

🔒 安全属性（已正式验证）

Coq中证明的所有性能（见 .topos/SIGNAL_MCP_DECLARATIVE_SUCCESS_SPECIFICATION.md):

  1. E2EE：端到端加密（信号协议）
  2. 正向安全：删除双棘轮键
  3. 元数据保护：密封发件人
  4. 后量子安全：ML-KEM-1024（凯伯）
  5. 零知识：zkgroup匿名凭据

📦 安装

cargo add signal-mcp

或添加到 Cargo.toml:

[dependencies]
signal-mcp = "0.1"

🚀 快速开始

标准服务器（开发）

use signal_mcp::SignalMcpServer;
use tokio::io::{stdin, stdout};

#[tokio::main]
async fn main() -> anyhow::Result<()> {
    let server = SignalMcpServer::new();
    let transport = (stdin(), stdout());

    // Start MCP server
    server.serve(transport).await?;
    Ok(())
}

运行方式：

cargo run --example signal-server-stdio

HTTP SSE服务器（生产）

cargo run --features http-sse --release

🧪 测试

单元测试

cargo test

基于属性的测试（proptest）

cargo test --features verification

形式验证（Coq）

cd .topos/coq
coqc signal_mcp_verification.v

📐 形式验证

所有正式规范都单独存储在 .topos/:

验证工作流程

  1. 相空间转换 （非时间里程碑）：

    • 事件1：基金会成立
    • 事件2：翻译完成（Rust→ Coq通过锈蚀Coq）
    • 事件3-5：安全财产证明
    • 事件6：操作一致性
    • 事件7： SignalCPS成功 ✓

  2. 代表团运作结构:

    signal_encrypt_message delegates to:
  ├─ lookup_session (SessionStore)
  ├─ fetch_identity (IdentityKeyStore)
  ├─ compute_ciphertext (libsignal encrypt)
  └─ wrap_sealed_sender (sealed_sender_encrypt)

  3. BDD+依赖类型:

    Record TypedScenario (op: Operation) : Type := {
  given_state : PreconditionState;
  operation : op;
  then_state : PostconditionState op given_state  (* DEPENDENT! *)
}.

🎯 与现有解决方案的比较

功能 信号桌面 信号 信号MCP
LLM集成 ✗ ✗ ✓ 原生
批量操作 有限 有限 ✓ 随着进展
加密透明 隐藏 部分 ✓ Full
会话反思 ✗ 有限 ✓ 完成
正式验证 ✗ ✗ ✓ Coq证明
安全验证UX 手册 手册 ✓ 引出
OAuth ✗ ✗ ✓ MCP 2025-06-18
实时流媒体 WebSocket WebSocket ✓ HTTP SSE

📊 平衡三元种子1069

验证种子： [+1, -1, -1, +1, +1, +1, +1]

  • 7 trits → 7 建筑层
  • 17 = 1+0+6+9 → 17 结构线形
  • 69个认知时刻 → 渐进式证明结构

🤝 贡献

看 贡献.md 发展指南。

开发设置

git clone https://github.com/your-org/signal-mcp
cd signal-mcp
cargo build
cargo test

📝 许可证

仅限AGPL-3.0-请参阅 许可证 了解详情。

遵循Signal的许可：实现必须是开源的。

🔗 相关项目

📚 文档

🙏 致谢

  • 信号协议信号信使团队
  • 模型上下文协议的拟人化
  • 铁锈焦炭的正式土地
  • Topos分类地基研究所

状态：正式规范已完成，正在实施中

准备好了：活动1（基金会成立）→ 铁锈翻译的coq

成功标准：10/10已验证的特性（非时间持续时间）

∎

相关 MCP