CoSMed: a confidentiality-verified social media platform

DOI10.1007/S10817-017-9443-3zbMATH Open1451.68168OpenAlexW2775081510MaRDI QIDQ1663221FDOQ1663221

Franco Raimondi, Armando Pesenti Gritti, Andrei Popescu, Thomas Bauereiß

Publication date: 21 August 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/23357/1/cosmed_extended.pdf

zbMATH Keywords

formal verificationinteractive theorem provingIsabelle/HOLinformation flow securitysecure social media platform

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• A Brief Overview of Mizar
• Formal certification of code-based cryptographic proofs
• Isabelle/HOL. A proof assistant for higher-order logic
• Semi-intelligible Isar proofs from machine-generated proofs
• Concrete Semantics
• CakeML
• Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings
• Automated verification of selected equivalences for security protocols
• Constructive Type Classes in Isabelle
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Code Generation via Higher-Order Rewrite Systems
• A verified information-flow architecture
• Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21--24, 2015. Proceedings
• Truly Modular (Co)datatypes for Isabelle/HOL
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• CoSMed: A Confidentiality-Verified Social Media Platform
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• Encoding Monomorphic and Polymorphic Types

Cited In (1)

• CoCon: a conference management system with formally verified document confidentiality

Uses Software

• Isabelle
• Isabelle/HOL
• Isar
• Sledgehammer
• CakeML
• Locales
• ConfiChair
• seL4
• Jif
• CoSMed
• Ur/Web
• CAVA LTL Modelchecker
• FlowFox

Recommendations

• A Public-Key Protocol for Social Networks with Private Relationships 👍 👎
• CoSMed: A Confidentiality-Verified Social Media Platform 👍 👎

This page was built for publication: CoSMed: a confidentiality-verified social media platform

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663221)