Proof of Blowfish Cipher Algorithm

A proof is provided to show that the Blowfish decryption algorithm will give us back the original plaintext.

In previous tutorials, we have described both the Blowfish encryption algorithm and the decryption algorithm. Now let's try to approve that the decryption algorithm will actually give us back the original plaintext.

To help us to approve the decryption algorithm, we have to write the encryption algorithm and the decryption algorithm with temporary variables.

Encryption algorithm with temporary variables:

```Input:
T: 64 bits of clear text
P1, P2, ..., P18: 18 sub-keys
F(): Round function

Output:
C: 64 bits of cipher text

Algorithm - Blowfish Encryption:
(L0, R0) = T
L1 = L0 XOR P1
R2 = R0 XOR F(L1) XOR P2
L3 = L1 XOR F(R2) XOR P3
R4 = R2 XOR F(L3) XOR P4
L5 = L3 XOR F(R4) XOR P5
R6 = R4 XOR F(L5) XOR P6
L7 = L5 XOR F(R6) XOR P7
R8 = R6 XOR F(L7) XOR P8
L9 = L7 XOR F(R8) XOR P9
R10 = R8 XOR F(L9) XOR P10
L11 = L9 XOR F(R10) XOR P11
R12 = R10 XOR F(L11) XOR P12
L13 = L11 XOR F(R12) XOR P13
R14 = R12 XOR F(L13) XOR P14
L15 = L13 XOR F(R14) XOR P15
R16 = R14 XOR F(L15) XOR P16
L17 = L15 XOR F(R16) XOR P17
R18 = R16 XOR P18
C = (R18, L17)
```

Decryption algorithm with temporary variables:

```Input:
CC: 64 bits of cipher text
P1, P2, ..., P18: 18 sub-keys
F(): Round function

Output:
TT: 64 bits of clear text

Algorithm - Blowfish Decryption:
(LL0, RR0) = CC
LL1 = LL0 XOR P18
RR2 = RR0 XOR F(LL1) XOR P17
LL3 = LL1 XOR F(RR2) XOR P16
RR4 = RR2 XOR F(LL3) XOR P15
LL5 = LL3 XOR F(RR4) XOR P14
RR6 = RR4 XOR F(LL5) XOR P13
LL7 = LL5 XOR F(RR6) XOR P12
RR8 = RR6 XOR F(LL7) XOR P11
LL9 = LL7 XOR F(RR8) XOR P10
RR10 = RR8 XOR F(LL9) XOR P9
LL11 = LL9 XOR F(RR10) XOR P8
RR12 = RR10 XOR F(LL11) XOR P7
LL13 = LL11 XOR F(RR12) XOR P6
RR14 = RR12 XOR F(LL13) XOR P5
LL15 = LL13 XOR F(RR14) XOR P4
RR16 = RR14 XOR F(LL15) XOR P3
LL17 = LL15 XOR F(RR16) XOR P2
RR18 = R16 XOR P1
TT = (RR18, LL17)
```

Here is how to approve the decryption algorithm:

```Let:
T: 64 bits of plaintext
C: 64 bits of ciphertext encrypted from T
CC: 64 bits of ciphertext
TT: 64 bits of plaintext decrypted from CC

If:
CC = C

Then:
TT = T

Prove:
(LL0, RR0) = CC            Initializing step in decryption
= C                     Assumption of CC = C
= (R18, L17)            Finalizing step in encryption

LL1 = LL0 XOR P18          Applying P18 in decryption
= R18 XOR P18           Previous result
= R16 XOR P18 XOR P18   Applying P18 in encryption
= R16

RR2 = RR0 XOR F(LL1) XOR P17
Applying P17 in decryption
= L17 XOR F(R16) XOR P17
Previous result
Previous result
= L15 XOR F(R16) XOR P17 XOR F(R16) XOR P17
Applying P17 in encryption
= L15

......

LL17 = LL15 XOR F(RR16) XOR P2
Applying P2 in decryption
= R2 XOR F(L1) XOR P2
Previous result
= R0 XOR F(L1) XOR P2 XOR F(L1) XOR P2
Applying P2 in encryption
= R0

RR18 = RR16 XOR P1         Applying P1 in decryption
= L1 XOR P1             Previous result
= L0 XOR P1 XOR P1      Applying P1 in encryption
= L0

TT = (RR18, LL17)          Finalizing step in decryption
= (L0, R0)              Initializing step in encryption
= T
```

Last update: 2015.