Hi All,
since few months am using AVISPA. My main work is to model a specific
protocol for PANA fast re-authentication using context transfer.
am attaching my HLPSL model and also the relevant paper.
regarding this i ve some questions:
I test my model in many scenarios. Some of them show an attack. I list
all the scenarios here and i ll point where was the attack:
1) i test a singal session of the protocol
session(pac, npaa, cpaa, caaa, naaa)
there was no attack.
2) 2 sessions like:
a) session(pac, npaa, cpaa, caaa, naaa)
/\ session(i, npaa, cpaa, caaa, naaa)
b) session(pac, npaa, cpaa, caaa, naaa)
/\ session(pac, npaa, i, caaa, naaa)
c) session(pac, npaa, cpaa, caaa, naaa)
/\ session(pac, npaa, cpaa, i, naaa)
d) session(pac, npaa, cpaa, caaa, naaa)
/\ session(pac, npaa, cpaa, caaa, i)
e) session(pac, npaa, cpaa, caaa, naaa)
/\ session(pac, npaa, cpaa, caaa, naaa) % 2 similar sessions
in all the above scenarios (2.a - 2.d) there was no attack found.
f) session(pac, npaa, cpaa, caaa, naaa)
/\ session(pac, i, cpaa, caaa, naaa)
g) session(pac, npaa, cpaa, caaa, naaa)
/\ session(pac, cpaa, npaa, caaa, naaa) % replacing npaa and
cpaa with each other
in the scenarios 2.f and 2.g there was an attack found and by using
the -short option of the CL-AtSe shown to have a similar trace.
see the attached file named "attack.txt"
3) 4 sessions:
session(pac, npaa, cpaa, caaa, naaa)
/\ session(i, npaa, cpaa, caaa, naaa)
/\session(pac, i, cpaa, caaa, naaa)
/\ session(pac, npaa, i, caaa, naaa)
in this scenario also there is an attack found. see the "attack.txt"
othere thing when i ve used OFMC to check this scenario 2.b i found a
strange (for me) result, see the file "strange.txt".
it shows zero node are visited and 1000000 plies depth.
sorry for this long letter and many attachments. and thanx in advance..
with many regards
yours
Saleh