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的特性。