Abstract
Man-in-the-Middle (MM) is not only a ubiquitous attack pattern in security, but also an important paradigm of network computation and economics. Recognizing ongoing MM-attacks is an important security task; modeling MM-interactions is an interesting task for semantics of computation. Traced monoidal categories are a natural framework for MM-modelling, as the trace structure provides a tool to hide what happens in the middle. An effective analysis of what has been traced out seems to require an additional property of traces, called normality. We describe a modest model of network computation, based on partially ordered multisets (pomsets), where basic network interactions arise from the monoidal trace structure, and a normal trace structure arises from an iterative, i.e. coalgebraic structure over terms and messages used in computation and communication. The correspondence is established using a convenient monadic description of normally traced monoidal categories.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S.: Semantics of interaction: an introduction to game semantics. In: Dybjer, P., Pitts, A. (eds.) Proceedings of the 1996 CLiCS Summer School, Isaac Newton Institute, pp. 1–31. Cambridge University Press (1997)
Abramsky, S.: Interaction categories. In: Burn, G.L., Gay, S.J., Ryan, M. (eds.) Theory and Formal Methods, Workshops in Computing, pp. 57–69. Springer (1993)
Abramsky, S.: Algorithmic game semantics: A tutorial introduction. In: Schwichtenberg, H., Steinbrüggen, R. (eds.) Proceedings of the NATO Advanced Study Institute, Marktoberdorf, pp. 21–47. Kluwer Academic Publishers (2001)
Abramsky, S., Coecke, B.: A categorical semantics of quantum protocols. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society (2004); Also arXiv:quant-ph/0402130
Abramsky, S., Jagadeesan, R.: New foundations for the geometry of interaction. Information and Computation 111(1), 53–119 (1994)
Aczel, P., Adamek, J., Milius, S., Velebil, J.: Infinite trees and completely iterative theories: a coalgebraic view. Theor. Comput. Sci. 300(1-3), 1–45 (2003)
Adamek, J.: Introduction to coalgebra. Theory and Applications of Categories 14, 157–199 (2005)
Adamek, J., Milius, S., Velebil, J.: Free iterative theories: a coalgebraic view. Mathematical. Structures in Comp. Sci. 13(2), 259–320 (2003)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Anlauff, M., Pavlovic, D., Waldinger, R., Westfold, S.: Proving authentication properties in the Protocol Derivation Assistant. In: Degano, P., Küsters, R., Vigano, L. (eds.) Proceedings of FCS-ARSPA 2006. ACM (2006)
Bloom, S.L., Elgot, C.C.: The existence and construction of free iterative theories. J. Comput. Syst. Sci. 12(3), 305–318 (1976)
Bloom, S.L., Esik, Z.: Iteration theories: the equational logic of iterative processes. Springer-Verlag New York, Inc., New York (1993)
Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: Guttman, J. (ed.) Proceedings of CSFW 2005, pp. 48–61. IEEE (2005)
Datta, A., Derek, A., Mitchell, J., Pavlovic, D.: Secure protocol composition. E. Notes in Theor. Comp. Sci., pp. 87–114 (2003)
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)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system for security protocols and its logical formalization. In: Volpano, D. (ed.) Proceedings of CSFW 2003, pp. 109–125. IEEE (2003)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Secure protocol composition (extended abstract). In: Backes, M., Basin, D., Waidner, M. (eds.) Proceedings of FMCS 2003, pp. 11–23. ACM (2003)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: Abstraction and refinement in protocol derivation. In: Focardi, R. (ed.) Proceedings of CSFW 2004, pp. 30–47. IEEE (2004)
Diffie, W., van Oorschot, P.C., Wiener, M.J.: Authentication and authenticated key exchanges. Des. Codes Cryptography 2(2), 107–125 (1992)
Doctorow, C.: Solving and creating captchas with free porn, boingboing.net/2004/01/27/solving-and-creating.html (retrieved on January 2, 2012)
Durgin, N., Mitchell, J., Pavlovic, D.: A compositional logic for proving security properties of protocols. J. of Comp. Security 11(4), 677–721 (2004)
Durgin, N., Mitchell, J.C., Pavlovic, D.: A compositional logic for protocol correctness. In: Schneider, S. (ed.) Proceedings of CSFW 2001, pp. 241–255. IEEE (2001)
Pavlovic, D.: Geometry of abstraction in quantum computation. In: Mislove, M., Abramsky, S. (eds.) Clifford Lectures 2008, Proceedings of Symposia in Applied Mathematics, AMS, 28 p., arxiv.org:1006.1010 (2012)
Fabrega, J.T., Herzog, J., Guttman, J.: Strand spaces: Proving security protocols correct. J. Comp. Security 7(2/3), 191–230 (1999)
Girard, J.-Y.: Towards a geometry of interaction. In: Gray, J.W., Scedrov, A. (eds.) Categories in Computer Science and Logic. Contemporary Mathematics, vol. 92, pp. 69–108. American Mathematical Society (1989)
Gischer, J.L.: The equational theory of pomsets. Theor. Comp. Sci. 61(2-3), 199–224 (1988)
Hasegawa, M.: The uniformity principle on traced monoidal categories. Electr. Notes Theor. Comput. Sci. 69, 137–155 (2002)
Hyland, J.M.E., Luke Ong, C.-H.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)
Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 119(3), 447–468 (1996)
Kelsey, J., Schneier, B., Wagner, D.: Protocol Interactions and the Chosen Protocol Attack. In: Christianson, B., Crispo, B., Lomas, M., Roe, M. (eds.) Security Protocols 1997. LNCS, vol. 1361, pp. 91–104. Springer, Heidelberg (1998)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125–143 (1977)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
Lawvere, B.: Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America 50(1), 869–872 (1963)
MacLane, S.: Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics, vol. 5. Springer (1997)
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)
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 (2006)
Milner, R.: Action Calculi, or Syntactic Action Structures. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 105–121. Springer, Heidelberg (1993)
Milner, R.: Calculi for interaction. Acta Informatica 33(8), 707–737 (1996)
Moss, L.S.: Parametric corecursion. Theor. Comp. Sci. 260(1-2), 139–163 (2001)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21, 993–999 (1978)
Pavlovic, D.: Categorical logic of names and abstraction in action calculus. Math. Structures in Comp. Sci. 7, 619–637 (1997)
Pavlovic, D.: Network as a Computer: Ranking Paths to Find Flows. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) CSR 2008. LNCS, vol. 5010, pp. 384–397. Springer, Heidelberg (2008)
Pavlovic, D., Abramsky, S.: Specifying Interaction Categories. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 147–158. Springer, Heidelberg (1997)
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)
Pavlovic, D., Meadows, C.: Actor-Network Procedures. In: Ramanujam, R., Ramaswamy, S. (eds.) ICDCIT 2012. LNCS, vol. 7154, pp. 7–26. Springer, Heidelberg (2012)
Pratt, V.: Modelling concurrency with partial orders. Internat. J. Parallel Programming 15, 33–71 (1987)
Rivest, R.L., Shamir, A.: How to expose an eavesdropper. Commun. ACM 27, 393–394 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Pavlovic, D. (2012). Tracing the Man in the Middle in Monoidal Categories. In: Pattinson, D., Schröder, L. (eds) Coalgebraic Methods in Computer Science. CMCS 2012. Lecture Notes in Computer Science, vol 7399. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32784-1_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-32784-1_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32783-4
Online ISBN: 978-3-642-32784-1
eBook Packages: Computer ScienceComputer Science (R0)