```uclid
/* Alternating Bit Protocol Model in UCLID5 */

module main {
    type packet;
    type bit = boolean;

    /* State Definitions */
    const no_packet : packet;

    /* Channels */
    var st : [bit, packet];
    var message1 : [bit, packet];
    var message2 : [bit, packet];
    var ack : bit;

    /* Initialization */
    init {
        st = [false, no_packet];
        message1 = [false, no_packet];
        message2 = [false, no_packet];
        ack = false;
    }

    /* Transition System */
    next(st) {
        if (st[0] == ack) {
            return [!st[0], choose val: packet :: true]; // send new packet with flipped bit
        } else {
            return st; // resend same packet
        }
    }
    next(message1) {
        return *; // Non-deterministic loss or duplication
    }
    next(message2) {
        if (* && message1[0] == st[0]) {
            return message1; // Correct expected packet
        } else {
            return [!st[0], no_packet]; // otherwise, ignore or lose packet
        }
    }
    next(ack) {
        if (message2[0] == !st[0]) {
            return st[0]; // Accept and acknowledge last correct message
        } else {
            return *; // Non-deterministic loss or resend of acknowledgment
        }
    }

    /* Safety Properties */
    property valid_acknowledge {
        ack == st[0] => message2[0] == st[0] && message2[1] != no_packet;
    }

    property no_duplication {
        st[0] == ack -> st[1] != message2[1] || message2[1] == no_packet;
    }

    property progress {
        (eventually (ack == st[0]));
    }

    /* Engine Configuration */
    control {
        init;
        while (*) {
            next;
        }

        check;
    }
}

```
This UCLID5 model captures the essence of the alternating bit protocol over a non-reliable channel (with potential loss or duplication but no corruption). The `next` functions for `message1` and `ack` incorporate nondeterminism to simulate the unreliable nature of the channel. The safety properties check correct acknowledgment reception, prevention of message duplication under normal operation, and the guarantee that the protocol makes progress by eventually receiving the correct acknowledgment.