1、协议的形式化分析，前提是弄清楚协议结构和协议参与者之间的会话交互，以及会话之间使用的加解密算法，签名算法，认证算法，等牵扯的算法。之后便是将要分析的协议部分进行抽象化，具体抽象涉及协议参与者（发起者，承接着，转发着，接受者，等），协议使用的参数（参数包括，常量，变量，中间变量，演变量），协议使用的函数，抽象的步骤是按照协议参与者之间会话的顺序进行。协议的安全属性的声明是根据协议规范的要求来形式化。（好吧 感觉我说的是废话 呵呵哒）
TLS协议1.3版本的形式化中间牵扯很多的算法。所以首先要分析整个协议认证的过程。
下面是写的TLS1,3的伪代码（其中为简化需要，将复杂的函数全部简化成Hash算法代替）。。。。。。单是......实验结果证明，这个形式化的模型并不能验证TLS1.3，验证的安全属性全部结果存在攻击。（但是可以当做一个参考。在send_4.和send_5,6在剥离参数的时候分析应该还是跟原版本协议的要求存在不吻合，所以报错）
usertype Params,Sessionkey;
const Sign,Aenc,PR,hash:Function;
const Vesign,Adec,PU,unhash:Function;
inversekeys(Sign,Vesign);
inversekeys(Aenc,Adec);
inversekeys(PR,PU);
inversekeys(hash,unhash);
const Signkey,krsa:Sessionkey;
const PreSharedkey:Sessionkey;
macro clienthello=protocolversion,clietnrandom,ciphersuite,legacycompressionmethods,extension;
macro serverhello = protocolversion,serverrandom,ciphersuite;
macro encryptedextension=Aenc(presharedkey,PU(krsa));
macro serverencryptedextension=signaturealgorithm, Aenc(presharedkey,PU(krsa));
macro servercertificatedservername,certificate,PU(krsa) ;
macro signcertficate=servename,certificate,PU(krsa)),Sign(servername,certificate,PU(krsa)),PR(signkey);
macro randomcs=clietnrandom,ServerRandom;
const Alice,Bob,Eve:Agent;
protocol tls13(a,b){
role a{
fresh protocolversion,clietnrandom:Nonce;
fresh ciphersuite,legacycompressionmethods,extension:Nonce;
var serverrandom:Nonce;
var krsa:Sessionkey;
var signkey:Sessionkey;
var servername:Nonce;
var rresharedkey:Sessionkey;
var signaturealgorithm,certificate:Params;
send_1(a,b,protocolversion,clietnrandom,ciphersuite,legacycompressionmethods,extension);
recv_2(b,a,protocolversion,serverrandom,ciphersuite);
recv_3(b,a,signaturealgorithm,Aenc(presharedkey,PU(krsa)));
recv_4(b,a,servername,certificate,PU(krsa),Sign(servername,certificate,PU(krsa),PR(signkey)));
send_5(a,b,hash(hash((clienthello,encryptedextension,servercertificated),servercertificated)));
recv_6(b,a,hash(randomcs，hash((serverhello,serverencryptedextension,signcertficate),servercertificated));
claim_a1(a,Secret,presharedkey );
}
role b{
var ciphersuite,protocolversion,legacycompressionmethods,extension,clietnrandom:Nonce;
fresh servername,serverrandom:Nonce;
fresh krsa,signkey,presharedkey:Sessionkey;
fresh certificate,signaturealgorithm:Params;
var clietnRandom:Nonce;
recv_1(a,b,protocolversion,clietnrandom,ciphersuite,legacycompressionmethods,extension);
send_2(b,a,protocolversion,serverrandom,ciphersuite);
send_3(b,a,signaturealgorithm,Aenc(presharedkey,PU(krsa)));
send_4(b,a,servername,certificate,PU(krsa),Sign(servername,certificate,PU(krsa),PR(signkey)));
recv_5(a,b,hash(hash((clientHello,encryptedextension,servercertificated),servercertificated)));
send_6(b,a,hash(randomcs，hash((serverhello,serverencryptedextension,signcertficate),servercertificated));
claim_b1(b,Secret,presharedkey);
}
}附上 使我伤心欲绝的结果 今天是第四次实验失败（记录一哈 挫败感）
2、显然实验还是要做的 ，如何进行下去 ，，，，，，不能造假吧 ，，，我觉不行 长这么大我考试都从不抄的 ，
那么现在我开始怀疑是不是我的能力，、是不是还没有达到能分析清楚 1.3 ，，现在确实陷入困境，，实践是检验整理的唯一标准 ，读研最大的收获就是考验背的政治（是不是？），一套分析方法，
嗯，那就将1.2的再 重组，添加上1.3的特性。