296 research outputs found
Model Checking a Client-Side Micro Payment Protocol
No full textVirtual payment systems overcome the drawbacks such as processing and operational cost of the traditional payment system. The main aim of the virtual payment system is to provide efficient services in terms of cost. Online payment using credit card is one of the most expensive of all payment means. This gives advantage to micropayment systems where only small amounts are used for e-commerce. Payment which are small will be costly if paid through credit card. Therefore, there are several micropayment systems that exist and some have been proposed. One of the proposed micropayment system that this paper will talk about is Netpay. We will do model checking to check the correctness of this payment system and to see whether the protocol designers property claim is valid. Correctness is important in payment systems because money is involved in it, therefore the protocol needs to be validated. This paper examines the client-side version of the Netpay protocol and provides its formalization as a CSP model. The PAT model checker is used to prove three properties essential for correctness: impossibility of double spending, validity of an ecoin during the execution and the absence of deadlock. We prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative. This is a very strong assumption for system built to prevent abuse, but further analysis suggests that without it the protocol does no longer guarantee all correctness properties. We compare the two variation of the protocol with each other and with the properties claimed by the protocol designers
Twenty Percent and a Few Days – Optimising a Bitcoin Majority Attack
No full textBitcoin is a distributed online payment system that organises transactions into blocks. The size of blocks is limited to 1 megabyte, which also limits the number of transactions per second that can be confirmed. This year several attempts have been made to create a fork or a split that removes this restriction. One such alternative is Bitcoin Unlimited (BTU). Proponents of BTU have suggested to use a type of majority attack to force other Bitcoin miners to adopt BTU
A modified version of the ABC algorithm and evaluation of its performance
No full textThe artificial bee colony (ABC) optimization algorithm has been widely used to solve the global optimization problems. Many versions of ABC algorithm exist in the literature intending to achieve optimum solution for problems in different domains. Some modifications of the ABC algorithm are general and can be applied to any problem domain, while some are application dependent. This paper proposes a modified version of the ABC algorithm named as, MABC-SS (modified artificial bee colony algorithm with selection strategy), that can be applied to any problem domain. The algorithm is modified in terms of population initialization and update of a bee position using the old and a new food source equation based on the algorithm's performance in the previous iteration. The selection strategy is measured based on a novel approach called the rate of change. The population initialization in any optimization algorithm plays an important role in achieving the global optimum. The algorithm proposed in the paper uses random and an opposition-based learning technique to initialize the population and updates a bee's position after exceeding a certain number of trial limits. The rate of change is based on the average cost and is calculated for the past two iterations and compared for a method to be used in the current iteration to achieve the best result. The proposed algorithm is experimented with 35 benchmark test functions and 10 real world test functions. The findings indicate that the proposed algorithm is able to achieve the optimal result in most cases. The proposed algorithm is compared with the original ABC algorithm, modified versions of the ABC algorithm, and other algorithms in the literature using the test mentioned above. The parameters such as population size, number of iterations and runs were kept same for comparison with non-variants of ABC. In case of ABC variants, ABC specific parameters such as abandonment limit factor (0.6) and acceleration coefficient (1) were kept same. Results indicate that in 40% of the traditional benchmark test functions, the suggested algorithm works better than other variants of ABC (ABC, GABC, MABC, MEABC, BABC, and KFABC), while 30% of the traditional benchmark test functions are comparable. The proposed algorithm was compared to non-variants of ABC as well. The results show that the proposed algorithm achieved the best mean result in 50% of the CEC2019 benchmark test functions and in 94% of the classical benchmark test functions. The result is confirmed by Wilcoxon sum ranked test which shows that MABC-SS achieved statistically significant result in 48% of the classical and 70% of the CEC2019 benchmark test functions when compared with the original ABC. Overall, based on assessment and comparison in benchmark test functions used in this paper, the suggested algorithm is superior to others
The reality of media freedom in Swaziland under the new constitutional dispensation
No full textThe study concludes that there is still lack of media freedom in Swaziland under the new constitutional dispensation. Its significant finding is that the lack of media freedom is a consequence of constitutional, legal and extra-legal constraints
Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. Protocol
No full textThis paper considers on a network routing protocol known as Better Approach to Mobile Ad hoc Networks (B.A.T.M.A.N.). The protocol serves two aims: first, to discover all bidirectional links, and second, to identify the best-next-hop for every other node in the network. A key element is that each node will flood the network at regular intervals with so-called originator messages.This paper describes in detail a formalisation of the B.A.T.M.A.N. protocol. This exercise revealed several ambiguities and inconsistencies in the RFC. We developed two models. The first implements, if possible, a literal reading of the RFC, while the second model tries to be closer to the underlying concepts. The alternative model is in some places less restrictive, and rebroadcasts more often when it helps route discovery, and will on the other hand drop more messages that might interfere with the process.We verify for a basic untimed model that both interpretations ensure loop-freedom, bidirectional link discovery, and route-discovery. We use simulation of a timed model to compare the performance and found that both models are comparable when it comes to the time and number of messages needed for discovering routes. However, the alternative model identifies a significantly lower number of suboptimal routes, and thus improves on the literal interpretation of the RFC
Single Depot Multiple Travelling Salesman Problem Solved With Preference-Based Stepping Ahead Firefly Algorithm
No full textFirefly Algorithm (FA) mimics the flashing light characteristic of fireflies to solve optimization problems. An area where its utilization is limited is Travelling Salesman Problem (TSP). There are a number of algorithms utilized to solve the problem; however, there is still scope to do better in terms of solution quality. In this study, stepping ahead FA is proposed to solve the single depot Multiple Travelling Salesman Problem (MTSP) with threshold strategy. Rooted in the discrete FA (dFA), dFA-Step introduces a discrete transformation and threshold strategy to enhance optimization. The algorithm combines a unique stepping ahead mechanism with a threshold acceptance preference operator, achieving a balance between exploration and exploitation. The deterministic threshold acceptance approach facilitates the selection of sub-best solutions while the integration of neighborhood operators, like reverse cyclic permutation and swap transformation, enables exploration of solutions superior and closely aligned with the best solutions. The experimental results are compared with selected novel works from the literature where the results show competitive performance of the proposed algorithm in terms of solution quality. The proposed method gives insight in preference operator and stepping ahead mechanism for other researchers to utilize in discrete domains such as robotics and scheduling
An Even Better Approach – Improving the B.A.T.M.A.N. Protocol Through Formal Modelling and Analysis
No full textThis paper considers a network routing protocol known as Better Approach to Mobile Adhoc Networks (B.A.T.M.A.N.). The protocol has two aims: first, discovery of all bidirectional links, and second, identification of the best-next-hop to the other nodes. A key mechanism of the protocol is to flood the network at regular intervals with so-called originator messages.In previous work we formalised the B.A.T.M.A.N. protocol in Uppaal and found several ambiguities and inconsistencies [2]. More importantly, explicit choices in the RFC had, unfortunately, a negative impact on route discovery. This previous work compared a literal model based of the RFC with an incremental improvement. This paper goes one step further and proposes an alternative that departs from the RFC. We compare the performance using simulations in Uppaal, for static as well as dynamic topologies. The analysis shows that the proposed alternative reduces the number of suboptimal routes significantly, and recovers better from routing errors that are introduced by mobility
- …
