AN ENVIRONMENT FOR THE SPECIFICATION AND VERIFICATION OF TIME-DEPENDENT SECURITY PROTOCOLS

M. Benerecetti,∗ N. Cuomo,∗ and A. Peron∗

References

  1. [1] L. Vigan`o, Automated security protocol analysis with theAVISPA tool. Electronic Notes in Theoretical Computer Sci-ence, 155, 2006, 61–86.
  2. [2] J. Zhou & D. Gollmann, An efficient non-repudiation protocol,in PCSFW: Proc. of the 10th computer security foundationsworkshop, (IEEE Computer Society Press, 1997), Rockport,Massachusetts, USA.
  3. [3] E.M. Clarke, Automatic verification of finite-state concurrentsystems. in Logic in Computer Science (IEEE Computer So-ciety, 1994), Paris, France.
  4. [4] R. Alur, C. Courcoubetis, & D.L. Dill, Model-checking in densereal-time. Information and Computation, 104(1), 1993, 2–34.
  5. [5] A. Perrig, R. Canetti, J.D. Tygar, & D. Song, Efficientauthentication and signing of multicast streams over lossychannels, RSP: 21th IEEE Computer Society Symposium onResearch in Security and Privacy, San Diego, California, USA,2000.
  6. [6] M. Benerecetti, N. Cuomo, & A. Peron, Timed hlpsl forspecification and verification of time sensitive protocols, inJoint Workshop on Foundations of Computer Security andAutomated Reasoning for Security Protocol Analysis (FCS-ARSPA’06), Seattle, August 15–16, 2006, (Pierpaolo Degano,Ralf K¨usters, Luca Vigan`o, Steve Zdancewic), Seattle, Wash-ington, USA.
  7. [7] K.G. Larsen, P. Pettersson, & W. Yi, Uppaal in a Nutshell. In-ternational Journal on Software Tools for Technology Transfer,1(1–2), 1997, 134–152.
  8. [8] D. Dolev & A. Yao, On the security of public key protocols.IEEE Transactions on Information Theory, 29(2), 1983, 198–208.
  9. [9] M. Rusinowitch & M. Turuani, Protocol insecurity with a finitenumber of sessions and composed keys is NP-complete. TCS:Theoretical Computer Science, 299, 2003, 451–475.
  10. [10] J. Bengtsson & W. Yi, Timed automata: semantics, algorithmsand tools. In: J. Desel, W. Reisig & G. Rozenberg (Eds.),Lectures on concurrency and petri nets, 3098 of Lecture Notes inComputer Science (Springer, 2003), Berlin, Germany, 87–124.
  11. [11] M. Benerecetti, N. Cuomo, & A. Peron. Tpmc, A modelchecker for time–sensitive security protocols, The 2007 HighPerformance Computing and Simulation (HPCS’07) Conf.,June 4th – 6th, 2007, Prague, Czech Republic, 2007.
  12. [12] R. Gorrieri, E. Locatelli, & F. Martinelli, A simple languagefor real-time cryptographic protocol analysis, ESOP: 12thEuropean Symposium on Programming, Warsaw, Poland, 2003.
  13. [13] M. Napoli, M. Parente, & A. Peron, Specification and veri-fication of protocols with time constraints. Electronic NotesTheoretical Computer Science, 99, 2004, 205–227.
  14. [14] R.J. Corin, S. Etalle, P.H. Hartel, & A.H. Mader, Timedanalysis of security protocols. Journal of Computer Security,15(6), 2007, 619–645.191
  15. [15] G. Delzanno & P. Ganty, Automatic verification of time sensi-tive cryptographic protocols, Proc. of TACAS 2004, Barcelona,Spain, 2004, 342–356.
  16. [16] P. Broadfoot & G. Lowe, Analysing a stream authenticationprotocol using model checking. Proc. of ESORICS’02, LNCS2502, Zurich, Switzerland, 2002, 146–161.

Important Links:

Go Back