复算一次安全会话的握手、记录与重启 ​

完成这个实验后，你能从同一组公开测试材料生成握手transcript、方向与用途密钥和一条AEAD记录，再让发送计数与接收位图经过重启。每次接受或拒绝都能指出具体依据；删除方向标签、恢复旧计数和回滚接收窗口时，也能说明破坏的是哪一条性质。

下载完整Python检查器。它使用Python标准库的hashlib、hmac及已安装的cryptography库中的X25519、Ed25519、AESGCM、Argon2id；不访问网络、不连接真实服务、不读取用户凭据。所有固定私钥和“共享秘密”都是公开的合成测试数据，绝不可用于真实通信。

从哪里开始 ​

先会PRF理路伪随机函数Pseudorandom function · PRF由短密钥索引且对高效查询者不可与真随机函数区分的函数族。、MAC理路消息认证码Message authentication code · MAC用共享密钥生成并验证消息完整性标签的机制。、签名理路数字签名Digital signature由私钥签名、公开验证并提供不可伪造性的认证机制。、DH理路Diffie–Hellman 密钥交换Diffie–Hellman key exchange双方公开交换群幂并在离散对数型假设下导出共享秘密的协议。与AEAD理路认证加密Authenticated encryption · AE同时提供机密性与密文完整性的对称加密接口和安全目标。的接口即可。旧AEAD页保留nonce-respecting游戏和新鲜伪造定义，本实验直接使用它们。提取器与剩余哈希引理理路剩余哈希引理Leftover hash lemma · LHL二通用哈希把弱随机源压缩为公开种子和经典旁信息后仍接近均匀的输出，误差由平均条件最小熵控制；条件化与 Jensen 不等式给出证明，三比特例子精确算出联合距离。是另一条统计证明主线；本实验不声称HMAC-SHA256是适用于所有弱源的统计提取器。

使用Python 3.10或更新版本，并选用已经提供上述算法的cryptography环境。作者实际验证环境是cryptography 50.0.0；旧版本可能没有Argon2id，脚本会明确报缺失而不替换成玩具算法。普通运行输出检查摘要，加 --vectors 输出所有测试字节：

python foundations-secure-session-checker.py
python foundations-secure-session-checker.py --vectors

若缺依赖，应在你管理的测试环境中按库官方说明准备，不要用真实密钥替换公开样例。脚本不提供生产协议、密码库部署认证或完整TLS实现。

1. 把语义变成确定字节 ​

采用长度前缀编码理路密码协议字段的无歧义编码Cryptographic protocol field encoding · Length-delimited transcript encoding规定字段类型、长度和解析边界，用可逆编码把语义元组唯一映为认证字节，并拒绝截断、尾随及多重解释。E：两字节大端字段数，随后每个字段用四字节大端长度加原字节。固定字段与每字段65535字节上限；序号恰八字节。先手算 E(ab,c) 与 E(a,bc)，再让解析器拒绝截断、额外尾随字节和不匹配的字段数。

协议名为ASCII CS09-demo，版本 1，套件字符串为 X25519-Ed25519-HKDF-SHA256-AES128GCM；双方身份是 client.test、server.test。客户端DH私有输入字节依次为01至20（十六进制），服务端为21至40；签名私钥输入分别为41至60与61至80。公开随机数分别为00至0f与10至1f。这里用确定种子只为复算；它们不满足秘密随机源要求。

先得到两个32字节DH公钥X、Y和两个32字节签名公钥。把它们按如下顺序编码：

T0 = E(protocol, version, suite, client_id, server_id,
       client_nonce, server_nonce, X, Y, client_verify_key, server_verify_key)

T0的SHA-256应为：

9be9b549ddd5ffe8632cccd4df8deabdce0ac2fb9b0bab2bee11dd35e52421fe

检查器完整列出T0字节。可先检查字段数为11，再独立定位身份、DH公钥和签名公钥的边界，而不是只比较摘要。

2. 认证、派生与实际收到确认 ​

此实验把两个验证公钥预先绑定到测试身份；没有实现X.509。实际证书系统还需信任路径与期望服务名理路证书路径与期望服务身份Certificate path validation and service identity · Trust anchor and reference identity从外部信任锚出发验证证书路径与用途约束，再独立匹配期望服务身份，区分签名正确、路径有效和应用授权。检查。客户端与服务端分别签

E(protocol, version, client-auth, SHA256(T0))
E(protocol, version, server-auth, SHA256(T0))

引号表示字符串字段含义，不是编码中的额外字符。以固定顺序形成 T1=E(T0,client_signature,server_signature)。客户端与服务端分别做X25519，得到相同共享值Z；然后

salt = SHA256(E(protocol, version, client_nonce, server_nonce))
PRK = HKDF-Extract(salt, Z)
info = E(protocol, version, suite, client_id, server_id,
         direction, purpose, u16(output_length), transcript_hash)
key = HKDF-Expand(PRK, info, output_length)

先以 SHA256(T1) 为上下文、用途 finished、长度32派生c2s与s2c确认密钥。双方分别对 E(client-finished,SHA256(T1)) 和 E(server-finished,SHA256(T1)) 计算HMAC。确认消息分别为：

• 客户端：68146ad1c333dcbb7646e56e318cb7b25ba181b611b2e0de6edc32d9a17755ec
• 服务端：d0246386e7ba5d63b1caf26a6d6b760d7b3194e491069532358466ab23f58ea3

检查器有独立的Confirmation状态：身份和签名未验证时，先来的Finished不会建立会话；进入等待后，丢失Finished仍停在等待；错角色确认进入failed；只向客户端交付服务端确认时，只有客户端established。两端都接收正确确认后才各自建立。能够本地算出对方应发什么，与实际收到了持钥证据是两回事。

形成 Tf=E(T1,client_finished,server_finished)，其SHA-256为

56aa9f047fa1d78e055c156bce547b43487c889d760179316ba51eea62a14a43。

以该摘要为上下文、用途 application、长度16得到公开测试方向密钥：

• c2s：745c7195c95736720a238ea1c78b04c3
• s2c：c53786d57e6f75241a5c313261781bb9

删去info的方向字段，再以c2s、s2c调用同一个错误派生函数，两次结果严格相同。恢复字段后，此向量中的结果不同；一般随机输出仍可能偶然碰撞，理论主张是计算上的域分离而不是数学上永不相等。

3. 构造与接收一条真实记录 ​

本例采用显式序号和有限乱序模型。不是TLS1.3的隐式有序序号线格式。对c2s序号0，nonce为 000000000000000000000000，头部为

A = E(CS09-demo, 1, SHA256(Tf), c2s, data, u64(0))

明文为两个ASCII字节 m0。AES-128-GCM输出密文主体加16字节标签为

538b0f9175e4bc4b7bd22e73aa6cd6f7e3a8。

接收器核对期望协议、版本、会话摘要、方向和类型，再检查序号资格，认证成功后提交窗口并交付 m0。测试包括：改方向后认证失败，直接送往反方向接收器被头部门拒绝，改版本被拒绝；65535字节明文可接受，65536字节在发送端拒绝、即使有真实有效标签也在接收端按尺寸拒绝，短于16字节标签的记录同样拒绝。

记录层仍泄漏长度和公开头部，也不自动证明文件完整结束。若把最后一条记录丢弃，应用需要认证的总长度或终止条件才能识别截断。

4. 让发送端重启，让接收端乱序 ​

发送端先把排他上界D从0持久化到4，再使用0、1。此时崩溃后恢复到D=4，下一预留范围为[4,8)，实际使用序列为 0,1,4,5。未用2、3被丢弃，已用nonce没有重复。检查器穷举长度9的分配/崩溃事件序列，共512条；还检查预算为5时使用0至4后明确拒绝。

接收端使用宽度4的位图，依次输入合法序号 0,2,1,2,5,0,4，接受结果为：

接受，接受，接受，重复拒绝，接受，窗外拒绝，接受

最终最高序号5、位图1011。伪造序号99即使通过资格预检，认证失败后也不得推动窗口。恢复已保存窗口仍拒绝5；若错误地清空窗口却沿用旧会话密钥，旧记录0会再次被接受。检查器另穷举6种序号的长度5序列，共7776条，对照完整已接受集合与窗口左边界。

这里的持久化是抽象原子事件与内存快照，不是对磁盘、fsync、跨进程锁或断电硬件的测试。跨重启保留同一密钥和状态只是这个教学分支的假设；真实系统若不能防回滚/克隆，应拒绝续用或建立真正不同的新密钥。接收状态持久化与业务效果之间仍可能有崩溃窗口，本实验不承诺业务恰好执行一次。

5. 把故障放回对应的安全目标 ​

具体nonce复用反例使用 balance=100 与 balance=900。两明文的异或，以及两份GCM密文去掉16字节标签后的异或，都为 0000000000000000080000。这是实际算法输出，检查器没有以玩具异或算法冒充AEAD。

6. 三条独立安全分支 ​

口令分支复算Argon2id标准向量理路口令哈希、公开盐与内存成本Password hashing and salt · Memory-hard password verification定义被盗验证表下的离线猜测，分开公开盐、每猜测时间和内存难度，以Argon2id参数与标准向量检查可复算接口。，理解独立盐、每次猜测的时间与内存成本；该32 KiB小向量不是部署参数。HMAC/HKDF还先通过RFC4231 §4.2与RFC5869 A.1已公布结果，避免所有“参考值”都由自己的代码生成。

前向保密理路前向保密与秘密擦除Forward secrecy and erasure · Post-session long-term key compromise用会后长期密钥泄漏的测试游戏限定前向保密，区分临时秘密、会话密钥和认证密钥，并说明擦除与备份是必要实现假设。需分析会后长期认证密钥泄漏的游戏与真实擦除；公开固定种子实验不会证明它。CSPRNG理路熵源、CSPRNG状态与重播种CSPRNG state and reseeding · Entropy source and DRBG lifecycle分开物理熵输入与确定性生成状态，定义初始化、输出、更新和重播种，说明状态克隆、当前泄漏与未来恢复的不同保证。分支要求熵源、状态克隆与重播种模型，本实验不测系统随机源。常数时间理路常数时间的泄漏轨迹模型Constant-time leakage model · Cryptographic constant-time noninterference把分支、访存地址和变时操作数纳入跨秘密执行的观察，给出相同公开输出仍泄漏的反例，并界定编译器与硬件证明边界。分支需明确分支、地址和指令观察以及编译层级；本脚本没有机器代码验证或侧信道测试。

完成标准 ​

能独立解释E编码单射，按两块HMAC重算42字节HKDF，说明签名、Finished与应用密钥分别覆盖哪个transcript；能手算窗口1011与重启跳过2、3；能把每个失败归到字节解释、密钥域、安全游戏或状态不变量，而不把所有拒绝都叫“密码被破解”。

脚本当前提供25类断言组、512条分配崩溃轨迹和7776条窗口轨迹。它证明这些具体向量与有限模型检查通过，完整协议安全、真实持久化、证书库、熵源和侧信道保证都需要各自的额外证据。