A Dynamic Algebraic Specification for Social Networks

TL;DR

This paper formalizes social networks as algebraic objects using OTS and CafeOBJ, enabling formal verification of security properties to enhance safety in rapidly growing online social platforms.

Contribution

It introduces a novel formalization of social networks with OTS and CafeOBJ, allowing for rigorous security verification.

Findings

Successfully verified security properties of social networks

Demonstrated the applicability of formal methods in social network security

Enhanced confidence in social network safety through formal proofs

Abstract

With the help of the Internet, social networks have grown rapidly. This has increased security requirements. We present a formalization of social networks as composite behavioral objects, defined using the Observational Transition System (OTS) approach. Our definition is then translated to the OTS/CafeOBJ algebraic specification methodology. This translation allows the formal verification of safety properties for social networks via the Proof Score method. Finally, using this methodology we formally verify some security properties.