Skip to main content
SpringerLink
Log in

Actor-Network Procedures

(Extended Abstract)

  • Conference paper
Distributed Computing and Internet Technology (ICDCIT 2012)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 7154))

Abstract

In this paper we propose actor-networks as a formal model of computation in heterogenous networks of computers, humans and their devices, where these new procedures run; and we introduce Procedure Derivation Logic (PDL) as a framework for reasoning about security in actor-networks, as an extension of our previous Protocol Derivation Logic. Both formalisms are geared towards graphic reasoning. We illustrate its workings by analysing a popular form of two-factor authentication.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. of Cryptology 15(2), 103–127 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Anlauff, M., Pavlovic, D., Waldinger, R., Westfold, S.: Proving authentication properties in the Protocol Derivation Assistant. In: Proc. FCS-ARSPA 2006. ACM (2006)

    Google Scholar 

  3. Barthe, G., Hedin, D.L., Béguelin, S.Z., Grégoire, B., Heraud, S.: A machine-checked formalization of sigma-protocols. In: Proc. CSF 2010, pp. 246–260. IEEE Computer Society (2010)

    Google Scholar 

  4. Basin, D., Cremers, C., Meadows, C.: Model checking security protocols. In: Clarke, E., Henzinger, T., Veith, H. (eds.) Handbook of Model Checking. Springer, Heidelberg (to appear, 2011), http://people.inf.ethz.ch/cremersc/publications/index.html

    Google Scholar 

  5. Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Sec. Comput. 5(4), 193–207 (2008)

    Article  Google Scholar 

  6. Blaze, M.: Toward a Broader View of Security Protocols. In: Christianson, B., Crispo, B., Malcolm, J.A., Roe, M. (eds.) Security Protocols 2004. LNCS, vol. 3957, pp. 106–120. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Burrows, M.L., Abadi, M., Needham, R.: A Logic of Authentication. ACM Trans. Computer Systems 8(1), 18–36 (1990)

    Article  MATH  Google Scholar 

  8. Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: Proc. CSFW 2005, pp. 48–61. IEEE (2005)

    Google Scholar 

  9. Cortier, V., Kremer, S., Warinschi, B.: A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning 46(3-4), 225–259 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  10. Datta, A., Derek, A., Mitchell, J., Pavlovic, D.: Secure protocol composition. E. Notes in Theor. Comp. Sci., 87–114 (2003)

    Google Scholar 

  11. Datta, A., Derek, A., Mitchell, J., Pavlovic, D.: A derivation system and compositional logic for security protocols. J. of Comp. Security 13, 423–482 (2005)

    Article  Google Scholar 

  12. Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system for security protocols and its logical formalization. In: Proc. of CSFW 2003, pp. 109–125. IEEE (2003)

    Google Scholar 

  13. Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for Shapes in Cryptographic Protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  15. Dorogovtsev, S.N., Mendes, J.F.F.: Evolution of Networks: From Biological Nets to the Internet and WWW. Oxford University Press (2003)

    Google Scholar 

  16. Drimer, S., Murdoch, S.J., Anderson, R.: Optimised to Fail: Card Readers for Online Banking. In: Dingledine, R., Golle, P. (eds.) FC 2009. LNCS, vol. 5628, pp. 184–200. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Durgin, N., Mitchell, J., Pavlovic, D.: A compositional logic for proving security properties of protocols. J. of Comp. Security 11(4), 677–721 (2004)

    Article  Google Scholar 

  18. Durgin, N., Mitchell, J.C., Pavlovic, D.: A compositional logic for protocol correctness. In: Proc. of CSFW 2001, pp. 241–255. IEEE (2001)

    Google Scholar 

  19. Ellison, C.: Ceremony design and analysis. Cryptology ePrint Archive, Report 2007/399 (October 2007)

    Google Scholar 

  20. Thayer Fabrega, J., Herzog, J., Guttman, J.: Strand spaces: What makes a security protocol correct? Journal of Computer Security 7, 191–230 (1999)

    Article  Google Scholar 

  21. Gratzer, G.A.: Universal Algebra. Van Nostrand, Princeton (1968)

    MATH  Google Scholar 

  22. Hoepman, J.-H.: Ephemeral Pairing on Anonymous Networks. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 101–116. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  23. Karlof, C.S., Tygar, J.D., Wagner, D.: Conditioned-safe ceremonies and a user study of an application to web authentication. In: Proceedings of the 5th Symposium on Usable Privacy and Security, SOUPS 2009, p. 38:1 ACM (2009)

    Google Scholar 

  24. Kumar, A., Saxena, N., Tsudik, G., Uzun, E.: A comparative study of secure device pairing methods. Pervasive Mob. Comput. 5, 734–749 (2009)

    Article  Google Scholar 

  25. Latour, B.: Reassembling the Social: An Introduction to Actor-Network Theory. Oxford University Press (2005)

    Google Scholar 

  26. Laur, S., Nyberg, K.: Efficient Mutual Data Authentication Using Manually Authenticated Strings. In: Pointcheval, D., Mu, Y., Chen, K. (eds.) CANS 2006. LNCS, vol. 4301, pp. 90–107. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Laur, S., Pasini, S.: User-aided data authentication. IJSN 4(1/2), 69–86 (2009)

    Article  Google Scholar 

  28. Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1971)

    Book  MATH  Google Scholar 

  29. Meadows, C., Pavlovic, D.: Deriving, Attacking and Defending the GDOI Protocol. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 53–72. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  30. Meadows, C., Poovendran, R., Pavlovic, D., Chang, L., Syverson, P.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Poovendran, R., Wang, C., Roy, S. (eds.) Secure Localization and Time Synchronization in Wireless Ad Hoc and Sensor Networks. Springer, Heidelberg (2006)

    Google Scholar 

  31. Newman, M.: Networks: An Introduction. Oxford University Press (2010)

    Google Scholar 

  32. Nguyen, L.H., Roscoe, A.W.: Authentication protocols based on low-bandwidth unspoofable channels: a comparative survey. Journal of Computer Security (to appear, 2011)

    Google Scholar 

  33. Palsson, B.O.: Systems Biology: Properties of Reconstructed Networks. Cambridge University Press (2006)

    Google Scholar 

  34. Pasini, S., Vaudenay, S.: SAS-Based Authenticated Key Agreement. In: Yung, M., Dodis, Y., Kiayias, A., Malkin, T. (eds.) PKC 2006. LNCS, vol. 3958, pp. 395–409. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  35. Pavlovic, D.: Maps II: Chasing diagrams in categorical proof theory. J. of the IGPL 4(2), 1–36 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  36. Pavlovic, D., Meadows, C.: Deriving Secrecy in Key Establishment Protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 384–403. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  37. Pavlovic, D., Meadows, C.: Bayesian authentication: Quantifying security of the Hancke-Kuhn protocol. E. Notes in Theor. Comp. Sci. 265, 97–122 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  38. Pavlovic, D., Meadows, C.: Deriving ephemeral authentication using channel axioms. In: Proceedings of the Cambridge Workshop on Security Protocols 2009. Springer, Heidelberg (2010) (to appear)

    Google Scholar 

  39. Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: Proc. Automated Software Engineering 2001. IEEE (2001)

    Google Scholar 

  40. Pavlovic, D., Smith, D.R.: Guarded Transitions in Evolving Specifications. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 411–425. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  41. Peltz, C.: Web services orchestration and choreography. Computer 36, 46–52 (2003)

    Article  Google Scholar 

  42. Pieters, W.: Representing humans in system security models: An actor-network approach. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications 2(1), 75–92 (2011)

    Google Scholar 

  43. Pratt, V.: Modelling concurrency with partial orders. Internat. J. Parallel Programming 15, 33–71 (1987)

    Article  MATH  Google Scholar 

  44. Stajano, F., Wong, F.-L., Christianson, B.: Multichannel Protocols to Prevent Relay Attacks. In: Sion, R. (ed.) FC 2010. LNCS, vol. 6052, pp. 4–19. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  45. Vaudenay, S.: Secure Communications over Insecure Channels Based on Short Authenticated Strings. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 309–326. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. EWI/DIES, Royal Holloway, University of London and Universiteit Twente, UK

    Dusko Pavlovic

  2. Naval Research Laboratory, Code 5543, Washington, DC, 20375, USA

    Catherine Meadows

Authors
  1. Dusko Pavlovic
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Catherine Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Mathematical Sciences, C.I.T. Campus, Taramani, 600113, Chennai, India

    R. Ramanujam

  2. Industrial Software Systems, ABB Corporate Research Center, Bangalore, India

    Srini Ramaswamy

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pavlovic, D., Meadows, C. (2012). Actor-Network Procedures. In: Ramanujam, R., Ramaswamy, S. (eds) Distributed Computing and Internet Technology. ICDCIT 2012. Lecture Notes in Computer Science, vol 7154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28073-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28073-3_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28072-6

  • Online ISBN: 978-3-642-28073-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation