Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Purchase individual online access for 1 year to this journal.
Price: EUR 260.00Impact Factor 2024: 0.9
The Journal of Computer Security presents research and development results of lasting significance in the theory, design, implementation, analysis, and application of secure computer systems. It also provides a forum for ideas about the meaning and implications of security and privacy, particularly those with important consequences for the technical community.
The journal provides an opportunity to publish articles of greater depth and length than is possible in the proceedings of various existing conferences, while addressing an audience of researchers in computer security who can be assumed to have a more specialized background than the readership of other archival publications. The journal welcomes contributions on all aspects of computer security: confidentiality, integrity, and assurance of service - that is, protection against unauthorized disclosure or modification of sensitive information, or denial of service. Of interest is a precise understanding of security policies through modelling, as well as the design and analysis of mechanisms for enforcing them, and the architectural principles of software and hardware systems implementing them.
Authors: Hirschi, Lucca | Baelde, David | Delaune, Stéphanie
Article Type: Research Article
Abstract: In this paper, we consider the problem of verifying anonymity and unlinkability in the symbolic model, where protocols are represented as processes in a variant of the applied pi calculus, notably used in the ProVerif tool. Existing tools and techniques do not allow to verify directly these properties, expressed as behavioral equivalences. We propose a different approach: we design two conditions on protocols which are sufficient to ensure anonymity and unlinkability, and which can then be effectively checked automatically using ProVerif . Our two conditions correspond to two broad classes of attacks on unlinkability, i.e. data …and control-flow leaks. This theoretical result is general enough that it applies to a wide class of protocols based on a variety of cryptographic primitives. In particular, using our tool, UKano , we provide the first formal security proofs of protocols such as BAC and PACE (e-passport), Hash-Lock (RFID authentication), etc. Our work has also lead to the discovery of new attacks, including one on the LAK protocol (RFID authentication) which was previously claimed to be unlinkable (in a weak sense). Show more
Keywords: Formal verification, security protocols, symbolic model, equivalence-based properties
DOI: 10.3233/JCS-171070
Citation: Journal of Computer Security, vol. 27, no. 3, pp. 277-342, 2019
Authors: Zavatteri, Matteo | Viganò, Luca
Article Type: Research Article
Abstract: The workflow satisfiability problem is the problem of finding an assignment of users to tasks (i.e., a plan) so that all authorization constraints are satisfied. The workflow resiliency problem is a dynamic workflow satisfiability problem coping with the absence of users. If a workflow is resilient, it is of course satisfiable, but the vice versa does not hold. There are three levels of resiliency: in static resiliency, up to k users might be absent before the execution starts and never become available for that execution; in decremental resiliency, up to k users might …be absent before or during execution and, again, they never become available for that execution; in dynamic resiliency, up to k users might be absent before executing any task and they may in general turn absent and available continuously, before or during the execution. Much work has been carried out to address static resiliency, little for decremental resiliency and, to the best of our knowledge, for dynamic resiliency no exact approach that returns a dynamic execution plan if and only if a workflow is resilient has been provided so far. In this paper, we tackle workflow resiliency via extended game automata . We provide three encodings (having polynomial-time complexity) from workflows to extended game automata to model each kind of resiliency as an instantaneous game and we use Uppaal-TIGA to synthesize a winning strategy (i.e., a controller) for such a game. If a controller exists, then the workflow is resilient (as the controller’s strategy corresponds to a dynamic plan). If it doesn’t, then the workflow is breakable . The approach that we propose is correct because it corresponds to a reachability problem for extended game automata (TCTL model checking). Moreover, we have developed Erre , the first tool for workflow resiliency that relies on a controller synthesis approach for the three kinds of resiliency. Thanks to Erre , our approach is thus also fully-automated from analysis to simulation. Show more
Keywords: Workflow satisfiability and resiliency, resource allocation under uncertainty, high availability, extended game automata, dynamic controllability, unbreakable security, AI-based security, formal methods
DOI: 10.3233/JCS-181244
Citation: Journal of Computer Security, vol. 27, no. 3, pp. 343-373, 2019
Authors: Yu, Xingjie | Thang, Michael Shiwen | Li, Yingjiu | Deng, Robert Huijie
Article Type: Research Article
Abstract: In Bitcoin network, the distributed storage of multiple copies of the block chain opens up possibilities for double-spending, i.e., a payer issues two separate transactions to two different payees transferring the same coins. While Bitcoin has inherent security mechanism to prevent double-spending attacks, it requires a certain amount of time to detect the double-spending attacks after the transaction has been initiated. Therefore, it is impractical to protect the payees from suffering in double-spending attacks in fast payment scenarios where the time between the exchange of currency and goods or services is shorten to few seconds. Although we cannot prevent double-spending …attacks immediately for fast payments, decentralized non-equivocation contracts have been proposed to penalize the malicious payer after the attacks have been detected. The basic idea of these contracts is that the payer locks some coins in a deposit when he initiates a transaction with the payee. If the payer double-spends, a cryptographic primitive called accountable assertions can be used to reveal his Bitcoin credentials for the deposit. Thus, the malicious payer could be penalized by the loss of deposit coins. However, such decentralized non-equivocation contracts are subjected to collusion attacks where the payer colludes with the beneficiary of the depoist and transfers the Bitcoin deposit back to himself when he double-spends, resulting in no penalties. On the other hand, even if the beneficiary behaves honestly, the victim payee cannot get any compensation directly from the deposit in the original design. To prevent such collusion attacks, we design fair time-locked deposits for Bitcoin transactions to defend against double-spending. The fair deposits ensure that the payer will be penalized by the loss of his deposit coins if he double-spends and the victim payee’s loss will be compensated within a locked time period. We start with the protocols of making a deposit for one transaction. In particular, for the transaction with single input and output and the transaction with multiple inputs and outputs, we provide different designs of the deposits. We analyze the performance of deposits made for one transaction and show how the fair deposits work efficiently in Bitcoin. We also provide protocols of making a deposit for multiple transactions, which can reduce the burdens of a honest payer. In the end, we extend the fair deposits to non-equivocation contracts for other distributed systems. Show more
Keywords: Bitcoin, fair deposit, double-spending, collusion attacks, time-locked
DOI: 10.3233/JCS-191274
Citation: Journal of Computer Security, vol. 27, no. 3, pp. 375-403, 2019
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl