@inproceedings{alturki19cathy, author = {Alturki, Musab A. and Ban Kirigin, Tajana and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {11565}, pages = {192--213}, year = {2019}, } @conference{, author = {Alturki, Musab A. and Ban Kirigin, Tajana and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, series = {LNCS}, number = {11565}, pages = {192--213}, year = {2019}, doi = {10.1007/978-3-030-19052-1}, } @inproceedings{urquiza19csf, author = {Aires Urquiza, Abra{\~{a}}o and Alturki, Musab A. and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre}, title = {Resource-Bounded Intruders in Denial of Service Attacks}, booktitle = {32nd {IEEE} Computer Security Foundations Symposium, {CSF} 2019, Hoboken, NJ, USA, June 25-28, 2019}, publisher = {{IEEE}}, pages = {382--396}, year = {2019}, doi = {10.1109/CSF.2019.00033}, } @article{DBLP:journals/mscs/KanovichKNS19, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {Subexponentials in non-commutative linear logic}, journal = {Mathematical Structures in Computer Science}, volume = {29}, number = {8}, pages = {1217--1249}, year = {2019}, doi = {10.1017/S0960129518000117}, url = {https://doi.org/10.1017/S0960129518000117}, } @inproceedings{kanovich18ijcar, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {A Logical Framework with Commutative and Non-commutative Subexponentials}, booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings}, pages = {228--245}, year = {2018}, abstract = {Logical frameworks allow the specification of deductive systems usingthe same logical machinery. Linear logical frameworks have been successfullyused for the specification of a number of computational, logics and proofsystems. Its success relies on the fact that formulas can be distinguished as linear,which behave intuitively as resources, and unbounded, which behave intuitionistically.Commutative subexponentials enhance the expressiveness of linear logicframeworks by allowing the distinction of multiple contexts. These contexts maybehave as multisets of formulas or sets of formulas. Motivated by applicationsin distributed systems and in type-logical grammar, we propose a linear logicalframework containing both commutative and non-commutative subexponentials.Non-commutative subexponentials can be used to specify contexts which behaveas lists, not multisets, of formulas. In addition, motivated by our applications intype-logical grammar, where the weakenening rule is disallowed, we investigatethe proof theory of formulas that can only contract, but not weaken. In fact, ourcontraction is non-local. We demonstrate that under some conditions such formulasmay be treated as unbounded formulas, which behave intuitionistically.}, doi = {10.1007/978-3-319-94205-6\_16}, url = {https://doi.org/10.1007/978-3-319-94205-6\_16}, } @inproceedings{kanovich18fcs, author = {Alturki, Musab A. and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols.}, booktitle = {"Workshop on Foundations of Computer Security"}, year = {2018}, abstract = {Distance-bounding (DB) protocols were proposed tothwart relay attacks on proximity-based access control systems.In a DB protocol, the verifier computes an upper bound on thedistance to the prover by measuring the time needed for a signalto travel to the prover and back. DB protocols are, however,vulnerable to distance fraud, in which a dishonest prover isable to manipulate the distance bound computed by an honestverifier. Despite their conceptual simplicity, devising a formalcharacterization of DB protocols and distance fraud attacks thatis amenable to automated formal analysis is non-trivial, primarilybecause of their real-time and probabilistic nature. In this work,we present a framework, based on rewriting logic, for formallyanalyzing different forms of distance-fraud, including recentlyidentified timing attacks. We introduce a generic, real-time andprobabilistic model of DB protocols and use it to (mechanically)verify false-acceptance and false-rejection probabilities undervarious settings and attacker models through statistical modelchecking with MAUDE and PVESTA. Using this framework,we first accurately confirm known results and then define andquantitatively evaluate new guessing-ahead attack strategies thatwould otherwise be difficult to analyze manually.}, } @article{kanovich18mscs, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {Subexponentials in non-commutative linear logic}, journal = {Mathematical Structures in Computer Science}, year = {2018}, abstract = {Linear logical frameworks with subexponentials have been used for the specification of,among other systems, proof systems, concurrent programming languages and linearauthorisation logics. In these frameworks, subexponentials can be configured to allow or notfor the application of the contraction and weakening rules while the exchange rule canalways be applied. This means that formulae in such frameworks can only be organised assets and multisets of formulae not being possible to organise formulae as lists of formulae.This paper investigates the proof theory of linear logic proof systems in thenon-commutative variant. These systems can disallow the application of exchange rule onsome subexponentials. We investigate conditions for when cut elimination is admissible inthe presence of non-commutative subexponentials, investigating the interaction of theexchange rule with the local and non-local contraction rules. We also obtain some newundecidability and decidability results on non-commutative linear logic with subexponentials.}, doi = {10.1017/S0960129518000117}, url = {https://doi.org/10.1017/S0960129518000117}, } @article{DBLP:journals/mscs/KanovichKNSTP17, author = {Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Perovic, Ranko and Talcott, Carolyn}, editor = {Kr{\"{o}}ger, Torsten and Wahl, Friedrich M.}, title = {A rewriting framework and logic for activities subject to regulations}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {3}, pages = {332--375}, year = {2017}, abstract = {Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.}, doi = {10.1017/S096012951500016X}, url = {https://doi.org/10.1017/S096012951500016X}, } @article{DBLP:journals/jcs/KanovichKNST17, author = {Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Time, computational complexity, and probability in the analysis of distance-bounding protocols}, journal = {Journal of Computer Security}, volume = {25}, number = {6}, pages = {585--630}, year = {2017}, abstract = {Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with an attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.}, doi = {10.3233/JCS-0560}, url = {https://doi.org/10.3233/JCS-0560}, }