FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abstract Interpretation	Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
algorithm substitution attacks	Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (PDF, talk)
Attack Trees	Guided design of attack trees: a system-based approach (PDF, talk)
attacker knowledge	Assuming you know: epistemic semantics of relational annotations for expressive flow policies (PDF, talk)
Authentication	An extensive formal analysis of multi-factor authentication protocols (PDF, talk)
automated reasoning	Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk)
Automated verification	An extensive formal analysis of multi-factor authentication protocols (PDF, talk) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
B
backdoors	Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
Belenios	Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
bounds on leakage	Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
broadcast communication	A Cryptographic Look at Multi-Party Channels (PDF, talk)
C
causality preservation	A Cryptographic Look at Multi-Party Channels (PDF, talk)
composition	Composition Theorems for CryptoVerif and Application to TLS 1.3 (PDF, talk)
computational model	Composition Theorems for CryptoVerif and Application to TLS 1.3 (PDF, talk)
computational soundness	Symbolic security of garbled circuits (PDF, talk)
computer aided security proofs	Computer-aided proofs for multiparty computation with active security (PDF, talk)
computer-aided cryptography	Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
Confidentiality	A Cryptographic Look at Multi-Party Channels (PDF, talk) The Complexity of Monitoring Hyperproperties (PDF, talk)
cryptographic constant-time	Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (PDF, talk)
cryptographic schemes	Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (PDF, talk)
D
declassification	Assuming you know: epistemic semantics of relational annotations for expressive flow policies (PDF, talk)
Domain-specific languages	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
E
e-voting	Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk)
EasyCrypt	Formal Security Proof of CMAC and its Variants (PDF, talk) Computer-aided proofs for multiparty computation with active security (PDF, talk) Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
Ethereum	KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
F
Formal Analysis	An extensive formal analysis of multi-factor authentication protocols (PDF, talk)
Formal Methods	Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
formal methods for security	Symbolic security of garbled circuits (PDF, talk)
formal proof	Formal Security Proof of CMAC and its Variants (PDF, talk)
formal proofs	Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (PDF, talk)
formal verification	Composition Theorems for CryptoVerif and Application to TLS 1.3 (PDF, talk) Computer-aided proofs for multiparty computation with active security (PDF, talk) Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk)
G
garbled circuit	Symbolic security of garbled circuits (PDF, talk)
global states	A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (PDF, talk)
greatest fixed point	Symbolic security of garbled circuits (PDF, talk)
H
hash functions	Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
HKDF	Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
HMAC	Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
I
immunization	Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
Inductive invariants	Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
inference attacks	Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
information flow	The Complexity of Monitoring Hyperproperties (PDF, talk) Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk) Assuming you know: epistemic semantics of relational annotations for expressive flow policies (PDF, talk) A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk)
Information flow control	Types for Information Flow Control: Labeling Granularity and Semantic Models (PDF, talk)
integrity	A Cryptographic Look at Multi-Party Channels (PDF, talk)
K
kleptography	Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (PDF, talk) Backdoored Hash Functions: Immunizing HMAC and HKDF (PDF, talk)
knowledge-based noninterference	Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk)
L
language based security	A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk)
Log analysis	The Complexity of Monitoring Hyperproperties (PDF, talk)
M
MAC	Formal Security Proof of CMAC and its Variants (PDF, talk)
Machine Learning	Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
Modeling and Specification	KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
modelling secure protocols	Computer-aided proofs for multiparty computation with active security (PDF, talk)
Multi Factor	An extensive formal analysis of multi-factor authentication protocols (PDF, talk)
Multi-agent workflows	Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
Multi-party computation	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
N
Non-interference	Inductive Invariants for Noninterference in Multi-agent Workflows (PDF, talk)
O
operational semantics	KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
P
permission model	A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk)
Privacy	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk) Privacy Risk in Machine Learning: Analyzing the Connection to Overfitting (PDF, talk)
proactive security	Self-Guarding Cryptographic Protocols against Algorithm Substitution Attacks (PDF, talk)
propositional logic	Guided design of attack trees: a system-based approach (PDF, talk)
Protocol Verification	An extensive formal analysis of multi-factor authentication protocols (PDF, talk)
Q
quantitative information flow	Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
R
random sample voting	Alethea: A Provably Secure Random Sample Voting Protocol (PDF, talk)
reactive programs	Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk)
relative soundness results	A Typing Result for Stateful Protocols (PDF, talk)
robust declassification	Knowledge-based Security of Dynamic Secrets for Reactive Programs (PDF, talk)
runtime verification	The Complexity of Monitoring Hyperproperties (PDF, talk)
S
secure channels	A Cryptographic Look at Multi-Party Channels (PDF, talk)
Secure compilation	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk) Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time” (PDF, talk)
Secure multiparty computation	Computer-aided proofs for multiparty computation with active security (PDF, talk)
Security	Formal Security Proof of CMAC and its Variants (PDF, talk) Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
security definitions	Computer-aided proofs for multiparty computation with active security (PDF, talk)
security protocols	Composition Theorems for CryptoVerif and Application to TLS 1.3 (PDF, talk) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (PDF, talk) Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR (PDF, talk)
Semantic model	Types for Information Flow Control: Labeling Granularity and Semantic Models (PDF, talk)
semantics	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
side-channels	Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
Smart Contract Verification	KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (PDF, talk)
stateful protocols	A Typing Result for Stateful Protocols (PDF, talk)
symbolic constraints	A Typing Result for Stateful Protocols (PDF, talk)
symbolic cryptography	Symbolic security of garbled circuits (PDF, talk)
symbolic sampling	Symbolic Side-Channel Analysis for Probabilistic Programs (PDF, talk)
symbolic security	Symbolic security of garbled circuits (PDF, talk)
System-based design	Guided design of attack trees: a system-based approach (PDF, talk)
T
TLS	Composition Theorems for CryptoVerif and Application to TLS 1.3 (PDF, talk)
Trace semantics	Guided design of attack trees: a system-based approach (PDF, talk)
Translation	Types for Information Flow Control: Labeling Granularity and Semantic Models (PDF, talk)
type system	A Permission-Dependent Type System for Secure Information Flow Analysis (PDF, talk) Types for Information Flow Control: Labeling Granularity and Semantic Models (PDF, talk)
type systems	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk)
typing results	A Typing Result for Stateful Protocols (PDF, talk)
V
verifiable electronic voting	Machine-checked proofs for electronic voting: privacy and verifiability for Belenios (PDF, talk)
Verification	Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks (PDF, talk) A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif. (PDF, talk)

Disclaimer | Powered by EasyChair Smart Program