CoSMed: a confidentiality-verified social media platform

DOI10.1007/S10817-017-9443-3MaRDI QIDQ1663221zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• CoSMed: a confidentiality-verified social media platform
• A Public-Key Protocol for Social Networks with Private Relationships

Cites work

• A Brief Overview of Mizar
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• A verified information-flow architecture
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21--24, 2015. Proceedings
• Automated verification of selected equivalences for security protocols
• CakeML
• CoSMed: a confidentiality-verified social media platform
• Code generation via higher-order rewrite systems
• Concrete semantics. With Isabelle/HOL
• Constructive Type Classes in Isabelle
• Encoding monomorphic and polymorphic types
• Formal certification of code-based cryptographic proofs
• Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22--25, 2016. Proceedings
• Isabelle/HOL. A proof assistant for higher-order logic
• Java and the Java memory model -- a unified, machine-checked formalisation
• Semi-intelligible Isar proofs from machine-generated proofs
• Truly modular (co)datatypes for Isabelle/HOL

Cited in

(2)

• CoSMed: a confidentiality-verified social media platform
• CoCon: a conference management system with formally verified document confidentiality

Describes a project that uses

Uses Software

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

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)