FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

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

A
access control	IFCIL: An Information Flow Configuration Language for SELinux
adversarial contexts	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
adversarial robustness	Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems
attacker advantage	Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes
authenticated encryption	Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
authentication	Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
Automated proofs	A Complete Characterization of Security for Linicrypt Block Cipher Modes
availability	Applying consensus and replication securely with FLAQR
B
back-translation	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
bisimilarity	Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
Block cipher modes	A Complete Characterization of Security for Linicrypt Block Cipher Modes
blockchain	Contingent payments from two-party signing and verification for abelian groups
C
capabilities	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
capability machines	Proving full-system security properties under multiple attacker models on capability machines
Checked C	A Formal Model of Checked C
collusion-free protocols	Collusion-Preserving Computation without a Mediator
collusion-preserving protocols	Collusion-Preserving Computation without a Mediator
Compiler	A Formal Model of Checked C
Completeness	Prophecy Variables for Hyperproperty Verification
Computational Security	Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
computer-aided cryptography	Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
consensus	Applying consensus and replication securely with FLAQR
Coq	Adversary Safety by Construction in a Language of Cryptographic Protocols SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
covert channels	Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games
cryptography	Adversary Safety by Construction in a Language of Cryptographic Protocols
D
d-privacy	Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes
DDoS attacks	N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
decidability	A small bound on the number of sessions for security protocols
differential privacy	Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes The Complexity of Verifying Boolean Programs as Differentially Private
Digital ICs	Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
distance bounding	Is Eve nearby? Analysing protocols under the distant-attacker assumption
distant attacker	Is Eve nearby? Analysing protocols under the distant-attacker assumption
DP-3T	Privacy as Reachability
dynamic release	Towards a General-Purpose Dynamic Information Flow Policy
E
E-voting	Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
EKE	Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
electronic voting	How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis
equational theories	Contingent payments from two-party signing and verification for abelian groups
Ethereum 2.0	Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
F
fair exchange	Contingent payments from two-party signing and verification for abelian groups
formal methods	Privacy as Reachability Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
formal methods and verification	IFCIL: An Information Flow Configuration Language for SELinux N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
formal verification	Is Eve nearby? Analysing protocols under the distant-attacker assumption Contingent payments from two-party signing and verification for abelian groups Adversary Safety by Construction in a Language of Cryptographic Protocols Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co Proving full-system security properties under multiple attacker models on capability machines
full-system guarantees	Proving full-system security properties under multiple attacker models on capability machines
G
GDPR enforcement	DPL: A Language for GDPR Enforcement
H
hardware tokens	Collusion-Preserving Computation without a Mediator
Hyperliveness	Prophecy Variables for Hyperproperty Verification
HyperLTL	Prophecy Variables for Hyperproperty Verification
Hyperproperties	Prophecy Variables for Hyperproperty Verification Mapping Synthesis for Hyperproperties
I
Indistinguishability	Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
information flow	How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games
information flow control	IFCIL: An Information Flow Configuration Language for SELinux Towards a General-Purpose Dynamic Information Flow Policy
Information-flow security	Mapping Synthesis for Hyperproperties
Interactive Theorem Proving	Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
K
key agreement	Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
key exchange	Is Eve nearby? Analysing protocols under the distant-attacker assumption
key hierarchy	Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol
L
language-based mechanisms	DPL: A Language for GDPR Enforcement
language-based security	IFCIL: An Information Flow Configuration Language for SELinux
Legendre PRF	Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
Linicrypt	A Complete Characterization of Security for Linicrypt Block Cipher Modes
Linkability	Privacy as Reachability
Logic	Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
Logic Locking	Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
logical relations	Proving full-system security properties under multiple attacker models on capability machines
M
machine learning	Membership Inference Attacks against Classifiers
mechanized proofs	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
membership inference	Membership Inference Attacks against Classifiers
memory sharing	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
metric differential privacy	Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
multiparty computation	Collusion-Preserving Computation without a Mediator
multiset rewriting	Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
N
network security	N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
non-interactive key exchange	Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
noninterference	Towards a General-Purpose Dynamic Information Flow Policy
O
observational equivalence	Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
off-line guessing	Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
P
PAKE	Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
partial programs	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
path-aware Internet architectures	N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
preprocessing	Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
Privacy	How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co Membership Inference Attacks against Classifiers
privacy-utility trade-off	Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
Probabilistic model checking	Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems
probabilistic process equivalences	Symbolic protocol verification with dice: process equivalences in the presence of probabilities
Probabilistic programs	The Complexity of Verifying Boolean Programs as Differentially Private
proof techniques	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Prophecy Variables	Prophecy Variables for Hyperproperty Verification
protocol analysis	Adversary Safety by Construction in a Language of Cryptographic Protocols
Protocol security	Privacy as Reachability
protocols	Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments So near and yet so far: formal verification of distance bounding protocols
Q
quantum information	Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games
R
Refinement	Mapping Synthesis for Hyperproperties
replay attacks	How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis
replication	Applying consensus and replication securely with FLAQR
robust safety	Proving full-system security properties under multiple attacker models on capability machines
runtime checking	DPL: A Language for GDPR Enforcement
S
secure bandwidth allocation	N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
secure compilation	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
security	Locked Circuit Indistinguishability: A Notion of Security for Logic Locking So near and yet so far: formal verification of distance bounding protocols
security protocols	Is Eve nearby? Analysing protocols under the distant-attacker assumption Symbolic protocol verification with dice: process equivalences in the presence of probabilities A small bound on the number of sessions for security protocols Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
Selene	Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
SELinux	IFCIL: An Information Flow Configuration Language for SELinux
semantics	A Formal Model of Checked C
simulation	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Spatial Memory Safety	A Formal Model of Checked C
static analysis	A Formal Model of Checked C
stochastic systems	Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems
symbolic verification	Symbolic protocol verification with dice: process equivalences in the presence of probabilities
Symmetric key cryptography	A Complete Characterization of Security for Linicrypt Block Cipher Modes
Synthesis	Mapping Synthesis for Hyperproperties
T
tagged architectures	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Transition system	Privacy as Reachability
U
unforgeable pointers	SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
universal contracts	Proving full-system security properties under multiple attacker models on capability machines
universal optimality	Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
unlinkability	Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
V
vehicular platooning	Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol
Verification	Prophecy Variables for Hyperproperty Verification A small bound on the number of sessions for security protocols So near and yet so far: formal verification of distance bounding protocols
W
while programs	The Complexity of Verifying Boolean Programs as Differentially Private

Disclaimer | Powered by EasyChair Smart Program