FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

This page contains an index consisting of author-provided keywords.

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

Disclaimer | Powered by EasyChair Smart Program