scyther/gui/Protocols/IKE/jfki-core.spdl
Cas Cremers f9a34f4de5 BUGFIX: Updating hashfunction usage in protocol files to new conventions.
After the new function implementation, the 'Function' type is no longer one-way by default.
However, many protocol description files relied on this implicit assumption.
The solution is to use 'hashfunction' declarations instead to model one-wayness.

Original bug report by Binh Thanh Nguyen.
2014-01-08 15:13:16 +00:00

89 lines
1.2 KiB
Plaintext

# 1 "jfki-core.cpp"
# 1 "<command-line>"
# 1 "jfki-core.cpp"
# 15 "jfki-core.cpp"
# 1 "common.h" 1
hashfunction prf, KDF;
hashfunction g, h;
# 60 "common.h"
hashfunction H;
# 97 "common.h"
protocol @oracle (DH, SWAP) {
role DH {
var i, r: Nonce;
recv_!DH1( DH, DH, h(g(r),i) );
send_!DH2( DH, DH, h(g(i),r) );
}
role SWAP {
var i, r, Ni, Nr: Nonce;
# 150 "common.h"
recv_!SWAP1( SWAP, SWAP, KDF(h(g(r),i), Ni, Nr) );
send_!SWAP2( SWAP, SWAP, KDF(h(g(i),r), Ni, Nr) );
}
}
# 16 "jfki-core.cpp" 2
protocol jfki-core(I, R)
{
role I {
fresh i, Ni: Nonce;
var Nr: Nonce;
var Gr: Ticket;
send_1( I, R, Ni, I, g(i) );
recv_2( R, I, Nr, Ni, R, Gr, {Nr, Ni, Gr, g(i), I}sk(R) );
send_3( I, R, Nr, Ni, {Nr, Ni, Gr, g(i), R}sk(I) );
claim( I, SKR, KDF(h(Gr,i), Ni, Nr) );
claim( I, Alive );
claim( I, Weakagree );
}
role R {
fresh r, Nr: Nonce;
var Ni: Nonce;
var Gi: Ticket;
recv_1( I, R, Ni, I, Gi );
send_2( R, I, Nr, Ni, R, g(r), {Nr, Ni, g(r), Gi, I}sk(R) );
recv_3( I, R, Nr, Ni, {Nr, Ni, g(r), Gi, R}sk(I) );
claim( R, SKR, KDF(h(Gi,r), Ni, Nr) );
claim( R, Alive );
claim( R, Weakagree );
}
}