Bitcoin: Verification Using Agda and The Social Impacts of Bitcoin


In this project, we will try to get an understanding of the technology of Bitcoin and verify its integrity with the use of Agda to ensure that coins are secure. To this, we will also discuss the social aspects and how Bitcoin affects society.


The motivation for this project stems from my own interest in Bitcoins, other cryptocurrencies and security. I have tried to mine Bitcoin and a few other digital currencies in recent years which has pushed me to take up such a project.

Fundamentally, we can question whether the Bitcoin technology is safe since there are always malicious users who try to make money, regardless of the consequences, and become disruptive. What would happen if there is a fault with the underlying protocol? Maybe we can argue that Bitcoin may not be around forever, however, the block chain technology has many other uses in other niches in different sectors of the market.

To give a better understanding, Visa processes around 65,500 transactions per second [1] from 160 different currencies. In perspective to Bitcoin, the Bitcoin block chain processes around 267,000,000 transactions (As seen in figure 1) per day from one currency which is itself, Bitcoin. The graph shows us that the transactions are increasing monthly and maybe one day will supersede visa or even MasterCard. Figure 1: Bitcoin Transaction Chart Currently, we rely on a centralised organisation to whom keeps our money safe or at least we trust these organisations too keep our money safe. By them retaining our money, we can use electronic transactions to send money to a recipient allowing use to make purchases without the need to hand physical money over to a recipient. In the context of centralised organisations, Bitcoin is not centralised and is not some type of organisation. Bitcoin can be referred to as decentralised menaing that no body takes possession of the currency and is minted at a defined rate in the protocol. Bitcoin is a piece of software that is open source and anyone can download. Users can even edit the source code, such as change the algorithm and implement improvements such as smart contracts, to create their own cryptocurrency. The use of formal verification tools such as Agda, will show us if there are any problems with the Bitcoin protocol and to this we will get an understanding of how the technology functions. Also, we will get further understanding on how Bitcoin and other cryptocurrencies influence societies around us.

Project Aims

  • Analyse the social aspects of Bitcoin and other Cryptocurrencies.
  • Analyse the security of the block chain.
  • Formalise Bitcoin using Agda.

Background Information

Bitcoin was proposed by Satoshi Nakamoto, to which we derive the smallest value of Bitcoin called a Satoshi. Bitcoin is created to be annonymous so that nobody would be able to determine who sent and received a transaction. The anonymous feature stems from the cryptographic nature of the technology. Only the public keys are able to be viewed as a form of identity, however, seem to be useless on its own. An analogy would be the stock trading system where identities of sellers and buyers are not visible and only the times and sizes of the trades are shown to the public [Nak08]. Transactions get sent to a bitcoin address which begin with 1 or 3. The anonymousity is one of the main reasons to why Bitcoin is used. Bitcoin is also decentralised, that is, no central organisation owns the system but is rather distributed with a peer-to-peer system where miners mine blocks and confirm transactions and get rewarded in the process. Bitcoin is used by a vast amount of people. There are even celebrities that have decided to use, advertise and invest into Bitcoin. An example are the Winklevoss twins. The Winklevoss twins want to create a Bitcoin exchange but unfortunately was rejected due to insufficient regulation of Bitcoin [5].

Mining Bitcoins

Mining Bitcoins can be rewarding, that is, one must have a decent hardware set up to receive a profit. Due to the complexity of the cryptographic algorithm in use, to find a block takes quite a bit of processor power. Initially, Bitcoin was mined using CPU’s at mega hashes per second, until the mining was capable to be achieved using a GPU, which increased the hashing power exponentially to hundreds of mega hashes per second. Soon after, there were start-up companies claiming to have a SHA-256 (Bitcoins algorithm) ASIC in development, such as Avalon which produces power in the giga-hashes. Now the ASICS have been refined to produce Tera hashes per second. At that time, the difficulty to find a block was so high that it was just about profitable to mine. At the same time, the cost of mining hardware and electricity costs has started to result in negative return of investments due to an increasing difficulty unless the miners can buy more equipment, which is yet again, more cost.

Mining pools are very helpful for many reasons. They allow the mining of a block as a team, that is, once a block is mined in a mining pool, the earnings (Currently 12.5BTC) are distributed evenly to the number of shares that were submitted. This makes it easier for miners that have a relatively low hashing power where it may take months, years or even decades to find a block if they solo mined. The owners of the mining pool typically set fees therefore one must calculate if the fee taken is still profitable.

The Dark Web

The dark web can be a mischievous place on the internet. Typically, the dark web is referred to websites that cannot be accessed by using a usual web browser. Instead the websites must be accessed using The Onion Router (TOR) Network. If we look at Silk Road, there is a perfect example on how Bitcoins can be used to buy illegal items such as drugs, guns and other illegal material. Silk Road no longer exists thanks to FBI tax agent Gary Alford. Ross Ubricht allegedly was the owner and founder of Silk Road and was charged of money laundering, computer hacking and conspiracy to traffic narcotics. This led to the FBI to seize 26,000 Bitcoins and a further 144,000 Bitcoins later [4]. The use of Bitcoins due to its anonymity helped the development of Silk Road as FBI were unable to track where the transactions were going and coming from. Therefore, the FBI had no or very little evidence to convict people * Unordered List Itemor at least the ability to prevent criminals from doing further illegal activities.


Litecoin is the younger sibling of Bitcoin. Litecoin was developed by Charles Lee, an ex-software engineer at google making some alterations to the code and ultimately changing the cryptographic algorithm and all addresses to begin with L. This resulted in Litecoin to become one of the more popular cryptocurrencies. There are several ways that Litecoin is different to Bitcoin such as:

  • Unordered List ItemBitcoin has a block time of 10 minutes while Litecoin has a block time of 2.5 minutes. This results in faster confirmation times. Bitcoin would need approximately and hour to confirm a transaction (can be adjusted by changing a fee for the network) while bitcoin would take 15 minutes. This is ¼ of the time needed.
  • Unordered List ItemThere will only be 21 million Bitcoins however there will be 84 million Litecoins.

The cryptographic algorithms were changed from SHA-256 to Scrypt. This created a few problems with miners that decided to switch over to Litecoin since scrypt is very memory intensive and came to a point that FPGA’s, ASICS and CPU’s were not as good as GPU’s for mining this algorithm.

How Can Cryptocurrency and Blockchain Technology Play a Role in Building Social and Solidarity Finance?

In this paper, the researcher, Brett Scott, looks upon the potential of altcoins and how a digital currency can be created to solve financial problems. He starts his paper by looking at the current social reality of Bitcoin, comparing the use of Bitcoin in poorer countries for financial inclusion. Secondly, he attempts to look at the current attempts to create a cryptocurrency that is “based on explicitly cooperative and social justice principles” [6]. Thirdly, he considers the underlying technology of Bitcoin, the Blockchain 2.0. Brett Scott gives an example of how a bank electronic payment system currently works and uses the system to look at the similarities and differences in bitcoin. I can establish from his example that customers from a bank is has some sort of identifier, let’s call this a pin number. When we request a transaction, we must prove that we are who we say we are. Therefore, the pin is entered and that authenticates yourself. We could say that a bank has a database where our identifier has an allotted balance from the bank (which is the amount in your bank account) and that is retrieved after identifying. Since we have identified ourselves and authorised ourselves, we could request an amount to be withdrawn or sent to another bank account. Even if we withdraw, the funds are sent to another bank account. The problem that Brett lists is that this system will have to work by a “set of private intermediaries editing private databases that they hold”. The concept of Bitcoin being money is questioned and uses reference to our physical money to just being tokens, the same idea that Bitcoin takes since we hand over physical money such as cash or edit databases to transfer funds, like that way bitcoin sends transactions to another wallet. He continues to talk about Blockchain 2.0 technology and notes the possibility of changing code within the technology so that the Blockchain can be applied to other applications. An example described would be Ethereum with the smart contract facility. A fun activity mentioned is that a bed could be made on a Blockchain where two participants bet on the average level of rainfall over a certain period. The coins are sent to an escrow, which is maintained by the script and whichever address is correct, receives the coins [6].

How to Make a Mint: The Cryptography of Anonymous Electronic Cash.

This paper is written by Laurie Law, Susan Sabett, Jerry Solinas and they try to attempt to construct an electronic payment system modelled after our paper currency system. Even though the paper was published in 1996, the concepts of a cryptocurrency is present. To be specific, the ability for anonymous transactions. They started to discuss the potential of using digital signatures or what would become cryptography to facilitate in transactions to become anonymous however becomes worrisome for law authorities due to anonymity. Then they look at the negatives such as using the anonymous feature to partake in illegal activities such as drug trafficking. The researchers outlined the requirements of various security features, such as:

  • Privacy: To protect against eavesdropping.
  • User Identification: Protection against impersonation.
  • Message integrity: Protection against tampering or substitution so the message received is the same message that was sent.

It is stated that to ensure these are met, there would need to be some sort of wide scale use an authentication infrastructure. They proposed that this could be done with the use of encrypting messages using private keys. This leads into the topic that my paper is about; Bitcoin

Project Management

Applied Methodology

For my paper, I will be looking to apply the action research methodology which was recommended to me by my supervisor. Formally, we can describe this methodology as “an approach in which the action researcher and a client collaborate in the diagnosis of the problem and in the development of a solution based on the diagnosis” [7]. There are many advantages of action research such as both quantitate and qualitative data can be used as well is a great way to gain an in-depth knowledge about the problem. Action research consists of a spiral of following self-reflective cycles. The following outlines the cycles:

  1. Planning to initiate change [8]
  2. Act upon the change to start implementation also observe the process of implementation and consequences [8]
  3. Reflecting on processes of change and re-planning [8]
  4. Acting and observing [8]
  5. Reflecting [8]

Figure 2: Image to show process of action research [8]

Work Schedule

The chart produced above will contain a schedule to the allocation of my work for the project. I schedule to I can determine if the project is on track. Firstly, we see that I have to research Bitcoin. This is a fundamental part or a paper upon Bitcoin would not be able to be accomplished. Secondly, I have to learn Agda so that I can use the language to verify that the Bitcoin protocols are correct and don’t contain errors. Thirdly, my initial document needs to be submitted, marking my first milestone. The remainder for modelling is solely concerned with modelling separate parts of the system to create a complete model of Bitcoin. I would then have to present my work or the amount I have worked up to at Greg-y-nog. The submission of my dissertation would act as another milestone. Throughout this process, I am learning every step of the way.

Risk Analysis

The risks of an incomplete project are quite low. However, we will detail potential problems and if there is any technique or solution we can do to reduce the risk.

To begin, the following are potential risks:

  • I have set aims which are not achievable. This would create a project which is not feasible.
  • The verification is computationally impossible. This problem would be extremely unlikely.
  • Loss of data. Low chance but can happen dependent of age and usage of storage medium.
  • Illness and emergencies. I do have some medical issues meaning that the risk of an illness or emergency is slightly higher, however, I will endeavour to remain fit and healthy.
  • Unordered List ItemThe inability to complete the tasks set. This could mean that I am unable to create a verification of Bitcoin and instead will have to look at other aspects of Bitcoin.
  • Unordered List ItemPolitics and the Law; if Bitcoin were to become illegal then I will not be able to carry on with my project. However, there is almost no risk of this happening since the UK recognises Bitcoin.


[1] Visa Inc. Facts & Figures. 2017. Retrieved on October 31, 2017 from

[2] Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system.

[3] Bitcoin Mining. 2016. Retrieved on October 31, 2017 from

[4] Silk Road (Market Place). 2017. Retrieved on October 31, 2017 from

[5] John Detrixhe. 2017. The Winklevoss twins are making headway in their quest to get Wall Street to big on Bitcoin. Retrieved on October 31, 2017 from

[6] Brett Scott. 2016 How Can Cryptocurrency and Blockchain Technology Play a Role in Building Social and Solidarity Finance?

[7] Bryman, A. & Bell, E. 2011. “Business Research Methods” 3rd edition, Oxford University Press

[8] “Action research can be defined”. N.d. Retrieved on October 31, 2017 from:


QR Code
QR Code initial_document_bitcoin:social_impacts_of_bitcoin (generated for current page)